Theorem dfac12a

Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. (Contributed by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	dfac12a	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\in \mathrm{On}𝒫x\in \mathrm{dom}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢\mathrm{dom}\mathrm{card}\subseteq \mathrm{V}$$
2		eqss	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \left(\mathrm{dom}\mathrm{card}\subseteq \mathrm{V}\wedge \mathrm{V}\subseteq \mathrm{dom}\mathrm{card}\right)$$
3	1 2	mpbiran	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \mathrm{V}\subseteq \mathrm{dom}\mathrm{card}$$
4		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
5		unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
6	5	sseq1i	$$⊢\bigcup R_1\left[\mathrm{On}\right]\subseteq \mathrm{dom}\mathrm{card}\leftrightarrow \mathrm{V}\subseteq \mathrm{dom}\mathrm{card}$$
7	3 4 6	3bitr4i	$$⊢\mathrm{CHOICE}\leftrightarrow \bigcup R_1\left[\mathrm{On}\right]\subseteq \mathrm{dom}\mathrm{card}$$
8		dfac12r	$$⊢\forall x\in \mathrm{On}𝒫x\in \mathrm{dom}\mathrm{card}\leftrightarrow \bigcup R_1\left[\mathrm{On}\right]\subseteq \mathrm{dom}\mathrm{card}$$
9	7 8	bitr4i	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\in \mathrm{On}𝒫x\in \mathrm{dom}\mathrm{card}$$