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