Theorem dfac10c

Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal. (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	dfac10c	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists y\in \mathrm{On}y\approx x$$

Proof

Step	Hyp	Ref	Expression
1		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
2		eqv	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \forall xx\in \mathrm{dom}\mathrm{card}$$
3		isnum2	$$⊢x\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists y\in \mathrm{On}y\approx x$$
4	3	albii	$$⊢\forall xx\in \mathrm{dom}\mathrm{card}\leftrightarrow \forall x\exists y\in \mathrm{On}y\approx x$$
5	1 2 4	3bitri	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists y\in \mathrm{On}y\approx x$$