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

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

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 )