Theorem dfac10b

Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac ). (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	dfac10b	$$⊢\mathrm{CHOICE}\leftrightarrow \approx \left[\mathrm{On}\right]=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	elima	$$⊢x\in \approx \left[\mathrm{On}\right]\leftrightarrow \exists y\in \mathrm{On}y\approx x$$
3	2	bicomi	$$⊢\exists y\in \mathrm{On}y\approx x\leftrightarrow x\in \approx \left[\mathrm{On}\right]$$
4	3	albii	$$⊢\forall x\exists y\in \mathrm{On}y\approx x\leftrightarrow \forall xx\in \approx \left[\mathrm{On}\right]$$
5		dfac10c	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists y\in \mathrm{On}y\approx x$$
6		eqv	$$⊢\approx \left[\mathrm{On}\right]=\mathrm{V}\leftrightarrow \forall xx\in \approx \left[\mathrm{On}\right]$$
7	4 5 6	3bitr4i	$$⊢\mathrm{CHOICE}\leftrightarrow \approx \left[\mathrm{On}\right]=\mathrm{V}$$