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 ↔ ∀ 𝑥 ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		dfac10	⊢ ( CHOICE ↔ dom card = V )
2		eqv	⊢ ( dom card = V ↔ ∀ 𝑥 𝑥 ∈ dom card )
3		isnum2	⊢ ( 𝑥 ∈ dom card ↔ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )
4	3	albii	⊢ ( ∀ 𝑥 𝑥 ∈ dom card ↔ ∀ 𝑥 ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )
5	1 2 4	3bitri	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )