Theorem en4

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

	Ref	Expression
Assertion	en4	⊢ ( 𝐴 ≈ 4o → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝐴 = ( { 𝑥 , 𝑦 } ∪ { 𝑧 , 𝑤 } ) )

Proof

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