Theorem en2

Description: A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	en2	⊢ ( 𝐴 ≈ 2o → ∃ 𝑥 ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2	1	onordi	⊢ Ord 1o
3		df-2o	⊢ 2o = suc 1o
4		en1	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≈ 1o ↔ ∃ 𝑦 ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 } )
5	4	biimpi	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≈ 1o → ∃ 𝑦 ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 } )
6		df-pr	⊢ { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
7	6	enp1ilem	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 } → 𝐴 = { 𝑥 , 𝑦 } ) )
8	7	eximdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 } → ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } ) )
9	2 3 5 8	enp1i	⊢ ( 𝐴 ≈ 2o → ∃ 𝑥 ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } )