Metamath Proof Explorer

Theorem dfac12

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

Ref Expression
Assertion dfac12 ⊢ CHOICE ↔ ∀ x ∈ On 𝒫 ℵ ⁡ x ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 dfac12a ⊢ CHOICE ↔ ∀ y ∈ On 𝒫 y ∈ dom ⁡ card
2 dfac12k ⊢ ∀ y ∈ On 𝒫 y ∈ dom ⁡ card ↔ ∀ x ∈ On 𝒫 ℵ ⁡ x ∈ dom ⁡ card
3 1 2 bitri ⊢ CHOICE ↔ ∀ x ∈ On 𝒫 ℵ ⁡ x ∈ dom ⁡ card