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

Metamath Proof Explorer

Theorem dfac10c

Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion dfac10c ⊢ CHOICE ↔ ∀ x ∃ y ∈ On y ≈ x

Proof

Step Hyp Ref Expression
1 dfac10 ⊢ CHOICE ↔ dom ⁡ card = V
2 eqv ⊢ dom ⁡ card = V ↔ ∀ x x ∈ dom ⁡ card
3 isnum2 ⊢ x ∈ dom ⁡ card ↔ ∃ y ∈ On y ≈ x
4 3 albii ⊢ ∀ x x ∈ dom ⁡ card ↔ ∀ x ∃ y ∈ On y ≈ x
5 1 2 4 3bitri ⊢ CHOICE ↔ ∀ x ∃ y ∈ On y ≈ x