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 ↔ A B C = 3

Proof

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