This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝐴 = ( { 𝑥 , 𝑦 } ∪ { 𝑧 , 𝑤 } ) )