Description: A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | en3 | ⊢ ( 𝐴 ≈ 3o → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = { 𝑥 , 𝑦 , 𝑧 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2onn | ⊢ 2o ∈ ω | |
2 | df-3o | ⊢ 3o = suc 2o | |
3 | en2 | ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≈ 2o → ∃ 𝑦 ∃ 𝑧 ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 , 𝑧 } ) | |
4 | tpass | ⊢ { 𝑥 , 𝑦 , 𝑧 } = ( { 𝑥 } ∪ { 𝑦 , 𝑧 } ) | |
5 | 4 | enp1ilem | ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 , 𝑧 } → 𝐴 = { 𝑥 , 𝑦 , 𝑧 } ) ) |
6 | 5 | 2eximdv | ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 ∖ { 𝑥 } ) = { 𝑦 , 𝑧 } → ∃ 𝑦 ∃ 𝑧 𝐴 = { 𝑥 , 𝑦 , 𝑧 } ) ) |
7 | 1 2 3 6 | enp1i | ⊢ ( 𝐴 ≈ 3o → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = { 𝑥 , 𝑦 , 𝑧 } ) |