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	⊢ ( CHOICE ↔ ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ dom card ⊆ V
2		eqss	⊢ ( dom card = V ↔ ( dom card ⊆ V ∧ V ⊆ dom card ) )
3	1 2	mpbiran	⊢ ( dom card = V ↔ V ⊆ dom card )
4		dfac10	⊢ ( CHOICE ↔ dom card = V )
5		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
6	5	sseq1i	⊢ ( ∪ ( 𝑅1 “ On ) ⊆ dom card ↔ V ⊆ dom card )
7	3 4 6	3bitr4i	⊢ ( CHOICE ↔ ∪ ( 𝑅1 “ On ) ⊆ dom card )
8		dfac12r	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ ( 𝑅1 “ On ) ⊆ dom card )
9	7 8	bitr4i	⊢ ( CHOICE ↔ ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card )