You can and should go further: show that a cartesian $\ast$-autonomous category is indeed equivalent to a Boolean algebra. The proof is not very difficult.

@LSpice See Freyd's reminiscences of Eilenberg after his passing, here: ams.org/notices/199810/mem-eilenberg.pdf Freyd has told this in more than one place. My guess is that Eilenberg had in mind something broader than subscripts being a "tell" for tacit uses of choice; I'm not sure what it might be, but I like to think he would have approved this type of example as giving one reason to avoid subscripts when possible. Just as a matter of taste, I find that multiple indices often give notation a kind of thorny, cluttered look, and I am inclined to give Eilenberg's advice credence.

Sorry to have given offense, Alex; I thought it was a slip such as we are all prone to make. Of course, I did point it out earlier as well. I'll revert both our comments back.

Maybe it's not entirely clear to this poster that OP knows it outside of the example where $\Phi(0, \beta) = \aleph_\beta$. (By the way, it's possible that OP doesn't go by "he".)

The recent edit renders moot the opening three comments. I will probably delete these comments in a while.

@StefanWitzel One makes a choice at each successor stage, but you're right that AC as such is invoked at limit stages by assembling those infinite many prior choices. I don't think you're missing anything, and thanks for promoting clarity.

@LSpice Normally the way it works is that one says two statements are equivalent in the presence of given assumptions $A_1, \ldots, A_n$; in other words, one proves a statement of the form $(A_1 \wedge \ldots \wedge A_n) \Rightarrow (B \Leftrightarrow C)$. There's nothing very tricky about this -- all TFAE theorems are of this type. Similarly, a careful writer will write "in ZF, the axiom of choice and the well-ordering principle are equivalent".

I don't know, but "relegation" makes it sound like a demotion. It's not! Rota said somewhere that what mathematicians secretly want is a lemma named after them. Lucky Yoneda, lucky Nakayama. Results that, while they may be simple to prove, are profound and important by virtue of the fact they get used everyday by everyone in the field. I don't think it's outrageous to think of Farkas's lemma that way.

Very interesting. Some of it reminds me of what Rota said [in Indiscrete Thoughts] about Alfred Young (of Young tableaux fame): "Alfred Young's style of mathematical writing has unfortunately gone out of fashion: it is based on the assumption that the reader is to be treated as a gentleman with a sound mathematical education, and gentlemen need not be told the lowly details of proofs. As a consequence, we have to figure out certain inferences for which Young omits any explanation out of respect for his readers." [Of course, those papers are notorious nowadays for their apparent opacity.]

@GerryMyerson Thanks very much!