Theorem dfac10b

Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac ). (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	dfac10b	⊢ ( CHOICE ↔ ( ≈ “ On ) = V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elima	⊢ ( 𝑥 ∈ ( ≈ “ On ) ↔ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )
3	2	bicomi	⊢ ( ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 ↔ 𝑥 ∈ ( ≈ “ On ) )
4	3	albii	⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 ↔ ∀ 𝑥 𝑥 ∈ ( ≈ “ On ) )
5		dfac10c	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 )
6		eqv	⊢ ( ( ≈ “ On ) = V ↔ ∀ 𝑥 𝑥 ∈ ( ≈ “ On ) )
7	4 5 6	3bitr4i	⊢ ( CHOICE ↔ ( ≈ “ On ) = V )