Theorem en3

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

	Ref	Expression
Assertion	en3	⊢ ( 𝐴 ≈ 3o → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = { 𝑥 , 𝑦 , 𝑧 } )

Proof

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