This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↔ ∀ x ∈ On 𝒫 x ∈ 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 ⊢ ⋃ R1 On = V
6 5 sseq1i ⊢ ⋃ R1 On ⊆ dom ⁡ card ↔ V ⊆ dom ⁡ card
7 3 4 6 3bitr4i ⊢ CHOICE ↔ ⋃ R1 On ⊆ dom ⁡ card
8 dfac12r ⊢ ∀ x ∈ On 𝒫 x ∈ dom ⁡ card ↔ ⋃ R1 On ⊆ dom ⁡ card
9 7 8 bitr4i ⊢ CHOICE ↔ ∀ x ∈ On 𝒫 x ∈ dom ⁡ card