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

Metamath Proof Explorer

Theorem en2eqpr

Description: Building a set with two elements. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion en2eqpr ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≠ 𝐵 → 𝐶 = { 𝐴 , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2o ∈ ω
2 nnfi ⊢ ( 2o ∈ ω → 2o ∈ Fin )
3 1 2 ax-mp ⊢ 2o ∈ Fin
4 simpl1 ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ≈ 2o )
5 enfii ⊢ ( ( 2o ∈ Fin ∧ 𝐶 ≈ 2o ) → 𝐶 ∈ Fin )
6 3 4 5 sylancr ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ Fin )
7 simpl2 ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝐶 )
8 simpl3 ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝐶 )
9 7 8 prssd ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
10 enpr2 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
11 10 3expa ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
12 11 3adantl1 ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
13 4 ensymd ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 2o ≈ 𝐶 )
14 entr ⊢ ( ( { 𝐴 , 𝐵 } ≈ 2o ∧ 2o ≈ 𝐶 ) → { 𝐴 , 𝐵 } ≈ 𝐶 )
15 12 13 14 syl2anc ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 𝐶 )
16 fisseneq ⊢ ( ( 𝐶 ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ∧ { 𝐴 , 𝐵 } ≈ 𝐶 ) → { 𝐴 , 𝐵 } = 𝐶 )
17 6 9 15 16 syl3anc ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 )
18 17 eqcomd ⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 = { 𝐴 , 𝐵 } )
19 18 ex ⊢ ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≠ 𝐵 → 𝐶 = { 𝐴 , 𝐵 } ) )