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 e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> C e. W )
2 prfi 
 |-  { A , B } e. Fin
3 2 a1i 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> { A , B } e. Fin )
4 elprg 
 |-  ( C e. W -> ( C e. { 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 e. W -> ( C e. { A , B } <-> ( -. B =/= C \/ -. C =/= A ) ) )
14 13 biimpd 
 |-  ( C e. W -> ( C e. { A , B } -> ( -. B =/= C \/ -. C =/= A ) ) )
15 14 3ad2ant3 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( C e. { A , B } -> ( -. B =/= C \/ -. C =/= A ) ) )
16 15 imp 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ C e. { A , B } ) -> ( -. B =/= C \/ -. C =/= A ) )
17 16 olcd 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ C e. { A , B } ) -> ( -. A =/= B \/ ( -. B =/= C \/ -. C =/= A ) ) )
18 17 ex 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( C e. { 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 e. U /\ B e. V /\ C e. W ) -> ( C e. { 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 e. U /\ B e. V /\ C e. W ) -> ( C e. { A , B } -> -. ( A =/= B /\ B =/= C /\ C =/= A ) ) )
23 22 con2d 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> -. C e. { A , B } ) )
24 23 imp 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> -. C e. { A , B } )
25 hashunsng 
 |-  ( C e. W -> ( ( { A , B } e. Fin /\ -. C e. { A , B } ) -> ( # ` ( { A , B } u. { C } ) ) = ( ( # ` { A , B } ) + 1 ) ) )
26 25 imp 
 |-  ( ( C e. W /\ ( { A , B } e. Fin /\ -. C e. { A , B } ) ) -> ( # ` ( { A , B } u. { C } ) ) = ( ( # ` { A , B } ) + 1 ) )
27 1 3 24 26 syl12anc 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( # ` ( { A , B } u. { C } ) ) = ( ( # ` { A , B } ) + 1 ) )
28 simpr1 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> A =/= B )
29 3simpa 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( A e. U /\ B e. V ) )
30 29 adantr 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( A e. U /\ B e. V ) )
31 hashprg 
 |-  ( ( A e. U /\ B e. V ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
32 30 31 syl 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
33 28 32 mpbid 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( # ` { A , B } ) = 2 )
34 33 oveq1d 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( ( # ` { A , B } ) + 1 ) = ( 2 + 1 ) )
35 27 34 eqtrd 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( # ` ( { A , B } u. { C } ) ) = ( 2 + 1 ) )
36 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
37 36 fveq2i 
 |-  ( # ` { A , B , C } ) = ( # ` ( { A , B } u. { C } ) )
38 df-3 
 |-  3 = ( 2 + 1 )
39 35 37 38 3eqtr4g 
 |-  ( ( ( A e. U /\ B e. V /\ C e. W ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( # ` { A , B , C } ) = 3 )
40 39 ex 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( # ` { A , B , C } ) = 3 ) )
41 nne 
 |-  ( -. A =/= B <-> A = B )
42 hashprlei 
 |-  ( { B , C } e. Fin /\ ( # ` { B , C } ) <_ 2 )
43 prfi 
 |-  { B , C } e. Fin
44 hashcl 
 |-  ( { B , C } e. Fin -> ( # ` { B , C } ) e. NN0 )
45 44 nn0zd 
 |-  ( { B , C } e. Fin -> ( # ` { B , C } ) e. ZZ )
46 43 45 ax-mp 
 |-  ( # ` { B , C } ) e. ZZ
47 2z 
 |-  2 e. ZZ
48 zleltp1 
 |-  ( ( ( # ` { B , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { B , C } ) <_ 2 <-> ( # ` { B , C } ) < ( 2 + 1 ) ) )
49 2p1e3 
 |-  ( 2 + 1 ) = 3
50 49 a1i 
 |-  ( ( ( # ` { B , C } ) e. ZZ /\ 2 e. ZZ ) -> ( 2 + 1 ) = 3 )
51 50 breq2d 
 |-  ( ( ( # ` { B , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { B , C } ) < ( 2 + 1 ) <-> ( # ` { B , C } ) < 3 ) )
52 51 biimpd 
 |-  ( ( ( # ` { B , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { B , C } ) < ( 2 + 1 ) -> ( # ` { B , C } ) < 3 ) )
53 48 52 sylbid 
 |-  ( ( ( # ` { B , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { B , C } ) <_ 2 -> ( # ` { B , C } ) < 3 ) )
54 46 47 53 mp2an 
 |-  ( ( # ` { B , C } ) <_ 2 -> ( # ` { B , C } ) < 3 )
55 44 nn0red 
 |-  ( { B , C } e. Fin -> ( # ` { B , C } ) e. RR )
56 43 55 ax-mp 
 |-  ( # ` { B , C } ) e. RR
57 3re 
 |-  3 e. RR
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 } e. Fin /\ ( # ` { B , C } ) <_ 2 ) -> ( # ` { B , C } ) =/= 3 )
62 42 61 mp1i 
 |-  ( ( A e. U /\ B e. V /\ C e. 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 e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
69 41 68 sylbi 
 |-  ( -. A =/= B -> ( ( A e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
70 hashprlei 
 |-  ( { A , C } e. Fin /\ ( # ` { A , C } ) <_ 2 )
71 prfi 
 |-  { A , C } e. Fin
72 hashcl 
 |-  ( { A , C } e. Fin -> ( # ` { A , C } ) e. NN0 )
73 72 nn0zd 
 |-  ( { A , C } e. Fin -> ( # ` { A , C } ) e. ZZ )
74 71 73 ax-mp 
 |-  ( # ` { A , C } ) e. ZZ
75 zleltp1 
 |-  ( ( ( # ` { A , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , C } ) <_ 2 <-> ( # ` { A , C } ) < ( 2 + 1 ) ) )
76 49 a1i 
 |-  ( ( ( # ` { A , C } ) e. ZZ /\ 2 e. ZZ ) -> ( 2 + 1 ) = 3 )
77 76 breq2d 
 |-  ( ( ( # ` { A , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , C } ) < ( 2 + 1 ) <-> ( # ` { A , C } ) < 3 ) )
78 77 biimpd 
 |-  ( ( ( # ` { A , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , C } ) < ( 2 + 1 ) -> ( # ` { A , C } ) < 3 ) )
79 75 78 sylbid 
 |-  ( ( ( # ` { A , C } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , C } ) <_ 2 -> ( # ` { A , C } ) < 3 ) )
80 74 47 79 mp2an 
 |-  ( ( # ` { A , C } ) <_ 2 -> ( # ` { A , C } ) < 3 )
81 72 nn0red 
 |-  ( { A , C } e. Fin -> ( # ` { A , C } ) e. RR )
82 71 81 ax-mp 
 |-  ( # ` { A , C } ) e. RR
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 } e. Fin /\ ( # ` { A , C } ) <_ 2 ) -> ( # ` { A , C } ) =/= 3 )
87 70 86 mp1i 
 |-  ( ( A e. U /\ B e. V /\ C e. 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 e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
94 6 93 sylbi 
 |-  ( -. B =/= C -> ( ( A e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
95 hashprlei 
 |-  ( { A , B } e. Fin /\ ( # ` { A , B } ) <_ 2 )
96 hashcl 
 |-  ( { A , B } e. Fin -> ( # ` { A , B } ) e. NN0 )
97 96 nn0zd 
 |-  ( { A , B } e. Fin -> ( # ` { A , B } ) e. ZZ )
98 2 97 ax-mp 
 |-  ( # ` { A , B } ) e. ZZ
99 zleltp1 
 |-  ( ( ( # ` { A , B } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , B } ) <_ 2 <-> ( # ` { A , B } ) < ( 2 + 1 ) ) )
100 49 a1i 
 |-  ( ( ( # ` { A , B } ) e. ZZ /\ 2 e. ZZ ) -> ( 2 + 1 ) = 3 )
101 100 breq2d 
 |-  ( ( ( # ` { A , B } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , B } ) < ( 2 + 1 ) <-> ( # ` { A , B } ) < 3 ) )
102 101 biimpd 
 |-  ( ( ( # ` { A , B } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , B } ) < ( 2 + 1 ) -> ( # ` { A , B } ) < 3 ) )
103 99 102 sylbid 
 |-  ( ( ( # ` { A , B } ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` { A , B } ) <_ 2 -> ( # ` { A , B } ) < 3 ) )
104 98 47 103 mp2an 
 |-  ( ( # ` { A , B } ) <_ 2 -> ( # ` { A , B } ) < 3 )
105 96 nn0red 
 |-  ( { A , B } e. Fin -> ( # ` { A , B } ) e. RR )
106 2 105 ax-mp 
 |-  ( # ` { A , B } ) e. RR
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 } e. Fin /\ ( # ` { A , B } ) <_ 2 ) -> ( # ` { A , B } ) =/= 3 )
111 95 110 mp1i 
 |-  ( ( A e. U /\ B e. V /\ C e. 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 e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
118 9 117 sylbi 
 |-  ( -. C =/= A -> ( ( A e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
119 69 94 118 3jaoi 
 |-  ( ( -. A =/= B \/ -. B =/= C \/ -. C =/= A ) -> ( ( A e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
120 21 119 sylbi 
 |-  ( -. ( A =/= B /\ B =/= C /\ C =/= A ) -> ( ( A e. U /\ B e. V /\ C e. W ) -> ( # ` { A , B , C } ) =/= 3 ) )
121 120 com12 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( -. ( A =/= B /\ B =/= C /\ C =/= A ) -> ( # ` { A , B , C } ) =/= 3 ) )
122 121 necon4bd 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( # ` { A , B , C } ) = 3 -> ( A =/= B /\ B =/= C /\ C =/= A ) ) )
123 40 122 impbid 
 |-  ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )