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 ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )

Proof

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