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 ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C → A ≠ B → C = A B

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2 𝑜 ∈ ω
2 nnfi ⊢ 2 𝑜 ∈ ω → 2 𝑜 ∈ Fin
3 1 2 ax-mp ⊢ 2 𝑜 ∈ Fin
4 simpl1 ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → C ≈ 2 𝑜
5 enfii ⊢ 2 𝑜 ∈ Fin ∧ C ≈ 2 𝑜 → C ∈ Fin
6 3 4 5 sylancr ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → C ∈ Fin
7 simpl2 ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → A ∈ C
8 simpl3 ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → B ∈ C
9 7 8 prssd ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B ⊆ C
10 pr2nelem ⊢ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B ≈ 2 𝑜
11 10 3expa ⊢ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B ≈ 2 𝑜
12 11 3adantl1 ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B ≈ 2 𝑜
13 4 ensymd ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → 2 𝑜 ≈ C
14 entr ⊢ A B ≈ 2 𝑜 ∧ 2 𝑜 ≈ C → A B ≈ C
15 12 13 14 syl2anc ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B ≈ C
16 fisseneq ⊢ C ∈ Fin ∧ A B ⊆ C ∧ A B ≈ C → A B = C
17 6 9 15 16 syl3anc ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → A B = C
18 17 eqcomd ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C ∧ A ≠ B → C = A B
19 18 ex ⊢ C ≈ 2 𝑜 ∧ A ∈ C ∧ B ∈ C → A ≠ B → C = A B