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=AB

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→AB⊆C
10 enpr2 ⊢A∈C∧B∈C∧A≠B→AB≈2𝑜
11 10 3expa ⊢A∈C∧B∈C∧A≠B→AB≈2𝑜
12 11 3adantl1 ⊢C≈2𝑜∧A∈C∧B∈C∧A≠B→AB≈2𝑜
13 4 ensymd ⊢C≈2𝑜∧A∈C∧B∈C∧A≠B→2𝑜≈C
14 entr ⊢AB≈2𝑜∧2𝑜≈C→AB≈C
15 12 13 14 syl2anc ⊢C≈2𝑜∧A∈C∧B∈C∧A≠B→AB≈C
16 fisseneq ⊢C∈Fin∧AB⊆C∧AB≈C→AB=C
17 6 9 15 16 syl3anc ⊢C≈2𝑜∧A∈C∧B∈C∧A≠B→AB=C
18 17 eqcomd ⊢C≈2𝑜∧A∈C∧B∈C∧A≠B→C=AB
19 18 ex ⊢C≈2𝑜∧A∈C∧B∈C→A≠B→C=AB