Metamath Proof Explorer

Theorem hashtpg

Description: The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017) (Revised by AV, 18-Sep-2021)

Ref Expression
Assertion hashtpg ⊢A∈U∧B∈V∧C∈W→A≠B∧B≠C∧C≠A↔ABC=3

Proof

Step Hyp Ref Expression
1 simpl3 ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→C∈W
2 prfi ⊢AB∈Fin
3 2 a1i ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→AB∈Fin
4 elprg ⊢C∈W→C∈AB↔C=A∨C=B
5 orcom ⊢C=A∨C=B↔C=B∨C=A
6 nne ⊢¬B≠C↔B=C
7 eqcom ⊢B=C↔C=B
8 6 7 bitr2i ⊢C=B↔¬B≠C
9 nne ⊢¬C≠A↔C=A
10 9 bicomi ⊢C=A↔¬C≠A
11 8 10 orbi12i ⊢C=B∨C=A↔¬B≠C∨¬C≠A
12 5 11 bitri ⊢C=A∨C=B↔¬B≠C∨¬C≠A
13 4 12 bitrdi ⊢C∈W→C∈AB↔¬B≠C∨¬C≠A
14 13 biimpd ⊢C∈W→C∈AB→¬B≠C∨¬C≠A
15 14 3ad2ant3 ⊢A∈U∧B∈V∧C∈W→C∈AB→¬B≠C∨¬C≠A
16 15 imp ⊢A∈U∧B∈V∧C∈W∧C∈AB→¬B≠C∨¬C≠A
17 16 olcd ⊢A∈U∧B∈V∧C∈W∧C∈AB→¬A≠B∨¬B≠C∨¬C≠A
18 17 ex ⊢A∈U∧B∈V∧C∈W→C∈AB→¬A≠B∨¬B≠C∨¬C≠A
19 3orass ⊢¬A≠B∨¬B≠C∨¬C≠A↔¬A≠B∨¬B≠C∨¬C≠A
20 18 19 syl6ibr ⊢A∈U∧B∈V∧C∈W→C∈AB→¬A≠B∨¬B≠C∨¬C≠A
21 3ianor ⊢¬A≠B∧B≠C∧C≠A↔¬A≠B∨¬B≠C∨¬C≠A
22 20 21 syl6ibr ⊢A∈U∧B∈V∧C∈W→C∈AB→¬A≠B∧B≠C∧C≠A
23 22 con2d ⊢A∈U∧B∈V∧C∈W→A≠B∧B≠C∧C≠A→¬C∈AB
24 23 imp ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→¬C∈AB
25 hashunsng ⊢C∈W→AB∈Fin∧¬C∈AB→AB∪C=AB+1
26 25 imp ⊢C∈W∧AB∈Fin∧¬C∈AB→AB∪C=AB+1
27 1 3 24 26 syl12anc ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→AB∪C=AB+1
28 simpr1 ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→A≠B
29 3simpa ⊢A∈U∧B∈V∧C∈W→A∈U∧B∈V
30 29 adantr ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→A∈U∧B∈V
31 hashprg ⊢A∈U∧B∈V→A≠B↔AB=2
32 30 31 syl ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→A≠B↔AB=2
33 28 32 mpbid ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→AB=2
34 33 oveq1d ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→AB+1=2+1
35 27 34 eqtrd ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→AB∪C=2+1
36 df-tp ⊢ABC=AB∪C
37 36 fveq2i ⊢ABC=AB∪C
38 df-3 ⊢3=2+1
39 35 37 38 3eqtr4g ⊢A∈U∧B∈V∧C∈W∧A≠B∧B≠C∧C≠A→ABC=3
40 39 ex ⊢A∈U∧B∈V∧C∈W→A≠B∧B≠C∧C≠A→ABC=3
41 nne ⊢¬A≠B↔A=B
42 hashprlei ⊢BC∈Fin∧BC≤2
43 prfi ⊢BC∈Fin
44 hashcl ⊢BC∈Fin→BC∈ℕ0
45 44 nn0zd ⊢BC∈Fin→BC∈ℤ
46 43 45 ax-mp ⊢BC∈ℤ
47 2z ⊢2∈ℤ
48 zleltp1 ⊢BC∈ℤ∧2∈ℤ→BC≤2↔BC<2+1
49 2p1e3 ⊢2+1=3
50 49 a1i ⊢BC∈ℤ∧2∈ℤ→2+1=3
51 50 breq2d ⊢BC∈ℤ∧2∈ℤ→BC<2+1↔BC<3
52 51 biimpd ⊢BC∈ℤ∧2∈ℤ→BC<2+1→BC<3
53 48 52 sylbid ⊢BC∈ℤ∧2∈ℤ→BC≤2→BC<3
54 46 47 53 mp2an ⊢BC≤2→BC<3
55 44 nn0red ⊢BC∈Fin→BC∈ℝ
56 43 55 ax-mp ⊢BC∈ℝ
57 3re ⊢3∈ℝ
58 56 57 ltnei ⊢BC<3→3≠BC
59 54 58 syl ⊢BC≤2→3≠BC
60 59 necomd ⊢BC≤2→BC≠3
61 60 adantl ⊢BC∈Fin∧BC≤2→BC≠3
62 42 61 mp1i ⊢A∈U∧B∈V∧C∈W→BC≠3
63 tpeq1 ⊢A=B→ABC=BBC
64 tpidm12 ⊢BBC=BC
65 63 64 eqtr2di ⊢A=B→BC=ABC
66 65 fveq2d ⊢A=B→BC=ABC
67 66 neeq1d ⊢A=B→BC≠3↔ABC≠3
68 62 67 imbitrid ⊢A=B→A∈U∧B∈V∧C∈W→ABC≠3
69 41 68 sylbi ⊢¬A≠B→A∈U∧B∈V∧C∈W→ABC≠3
70 hashprlei ⊢AC∈Fin∧AC≤2
71 prfi ⊢AC∈Fin
72 hashcl ⊢AC∈Fin→AC∈ℕ0
73 72 nn0zd ⊢AC∈Fin→AC∈ℤ
74 71 73 ax-mp ⊢AC∈ℤ
75 zleltp1 ⊢AC∈ℤ∧2∈ℤ→AC≤2↔AC<2+1
76 49 a1i ⊢AC∈ℤ∧2∈ℤ→2+1=3
77 76 breq2d ⊢AC∈ℤ∧2∈ℤ→AC<2+1↔AC<3
78 77 biimpd ⊢AC∈ℤ∧2∈ℤ→AC<2+1→AC<3
79 75 78 sylbid ⊢AC∈ℤ∧2∈ℤ→AC≤2→AC<3
80 74 47 79 mp2an ⊢AC≤2→AC<3
81 72 nn0red ⊢AC∈Fin→AC∈ℝ
82 71 81 ax-mp ⊢AC∈ℝ
83 82 57 ltnei ⊢AC<3→3≠AC
84 80 83 syl ⊢AC≤2→3≠AC
85 84 necomd ⊢AC≤2→AC≠3
86 85 adantl ⊢AC∈Fin∧AC≤2→AC≠3
87 70 86 mp1i ⊢A∈U∧B∈V∧C∈W→AC≠3
88 tpeq2 ⊢B=C→ABC=ACC
89 tpidm23 ⊢ACC=AC
90 88 89 eqtr2di ⊢B=C→AC=ABC
91 90 fveq2d ⊢B=C→AC=ABC
92 91 neeq1d ⊢B=C→AC≠3↔ABC≠3
93 87 92 imbitrid ⊢B=C→A∈U∧B∈V∧C∈W→ABC≠3
94 6 93 sylbi ⊢¬B≠C→A∈U∧B∈V∧C∈W→ABC≠3
95 hashprlei ⊢AB∈Fin∧AB≤2
96 hashcl ⊢AB∈Fin→AB∈ℕ0
97 96 nn0zd ⊢AB∈Fin→AB∈ℤ
98 2 97 ax-mp ⊢AB∈ℤ
99 zleltp1 ⊢AB∈ℤ∧2∈ℤ→AB≤2↔AB<2+1
100 49 a1i ⊢AB∈ℤ∧2∈ℤ→2+1=3
101 100 breq2d ⊢AB∈ℤ∧2∈ℤ→AB<2+1↔AB<3
102 101 biimpd ⊢AB∈ℤ∧2∈ℤ→AB<2+1→AB<3
103 99 102 sylbid ⊢AB∈ℤ∧2∈ℤ→AB≤2→AB<3
104 98 47 103 mp2an ⊢AB≤2→AB<3
105 96 nn0red ⊢AB∈Fin→AB∈ℝ
106 2 105 ax-mp ⊢AB∈ℝ
107 106 57 ltnei ⊢AB<3→3≠AB
108 104 107 syl ⊢AB≤2→3≠AB
109 108 necomd ⊢AB≤2→AB≠3
110 109 adantl ⊢AB∈Fin∧AB≤2→AB≠3
111 95 110 mp1i ⊢A∈U∧B∈V∧C∈W→AB≠3
112 tpeq3 ⊢C=A→ABC=ABA
113 tpidm13 ⊢ABA=AB
114 112 113 eqtr2di ⊢C=A→AB=ABC
115 114 fveq2d ⊢C=A→AB=ABC
116 115 neeq1d ⊢C=A→AB≠3↔ABC≠3
117 111 116 imbitrid ⊢C=A→A∈U∧B∈V∧C∈W→ABC≠3
118 9 117 sylbi ⊢¬C≠A→A∈U∧B∈V∧C∈W→ABC≠3
119 69 94 118 3jaoi ⊢¬A≠B∨¬B≠C∨¬C≠A→A∈U∧B∈V∧C∈W→ABC≠3
120 21 119 sylbi ⊢¬A≠B∧B≠C∧C≠A→A∈U∧B∈V∧C∈W→ABC≠3
121 120 com12 ⊢A∈U∧B∈V∧C∈W→¬A≠B∧B≠C∧C≠A→ABC≠3
122 121 necon4bd ⊢A∈U∧B∈V∧C∈W→ABC=3→A≠B∧B≠C∧C≠A
123 40 122 impbid ⊢A∈U∧B∈V∧C∈W→A≠B∧B≠C∧C≠A↔ABC=3