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

Proof

Step	Hyp	Ref	Expression
1		dfac12a	⊢ ( CHOICE ↔ ∀ 𝑦 ∈ On 𝒫 𝑦 ∈ dom card )
2		dfac12k	⊢ ( ∀ 𝑦 ∈ On 𝒫 𝑦 ∈ dom card ↔ ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )
3	1 2	bitri	⊢ ( CHOICE ↔ ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )