MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashtpg Unicode version

Theorem hashtpg 12272
Description: The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
Assertion
Ref Expression
hashtpg

Proof of Theorem hashtpg
StepHypRef Expression
1 simpl3 993 . . . . . 6
2 prfi 7671 . . . . . . 7
32a1i 11 . . . . . 6
4 elprg 3975 . . . . . . . . . . . . . . . 16
5 orcom 387 . . . . . . . . . . . . . . . . 17
6 nne 2647 . . . . . . . . . . . . . . . . . . . 20
7 eqcom 2458 . . . . . . . . . . . . . . . . . . . 20
86, 7bitri 249 . . . . . . . . . . . . . . . . . . 19
98bicomi 202 . . . . . . . . . . . . . . . . . 18
10 nne 2647 . . . . . . . . . . . . . . . . . . 19
1110bicomi 202 . . . . . . . . . . . . . . . . . 18
129, 11orbi12i 521 . . . . . . . . . . . . . . . . 17
135, 12bitri 249 . . . . . . . . . . . . . . . 16
144, 13syl6bb 261 . . . . . . . . . . . . . . 15
1514biimpd 207 . . . . . . . . . . . . . 14
16153ad2ant3 1011 . . . . . . . . . . . . 13
1716imp 429 . . . . . . . . . . . 12
1817olcd 393 . . . . . . . . . . 11
1918ex 434 . . . . . . . . . 10
20 3orass 968 . . . . . . . . . 10
2119, 20syl6ibr 227 . . . . . . . . 9
22 3ianor 982 . . . . . . . . 9
2321, 22syl6ibr 227 . . . . . . . 8
2423con2d 115 . . . . . . 7
2524imp 429 . . . . . 6
26 hashunsng 12240 . . . . . . 7
2726imp 429 . . . . . 6
281, 3, 25, 27syl12anc 1217 . . . . 5
29 simpr1 994 . . . . . . 7
30 3simpa 985 . . . . . . . . 9
3130adantr 465 . . . . . . . 8
32 hashprg 12241 . . . . . . . 8
3331, 32syl 16 . . . . . . 7
3429, 33mpbid 210 . . . . . 6
3534oveq1d 6189 . . . . 5
3628, 35eqtrd 2490 . . . 4
37 df-tp 3964 . . . . 5
3837fveq2i 5776 . . . 4
39 df-3 10466 . . . 4
4036, 38, 393eqtr4g 2515 . . 3
4140ex 434 . 2
42 nne 2647 . . . . . . 7
43 hashprlei 12263 . . . . . . . . . 10
44 prfi 7671 . . . . . . . . . . . . . . 15
45 hashcl 12211 . . . . . . . . . . . . . . . 16
4645nn0zd 10830 . . . . . . . . . . . . . . 15
4744, 46ax-mp 5 . . . . . . . . . . . . . 14
48 2z 10763 . . . . . . . . . . . . . 14
49 zleltp1 10780 . . . . . . . . . . . . . . 15
50 2p1e3 10530 . . . . . . . . . . . . . . . . . 18
5150a1i 11 . . . . . . . . . . . . . . . . 17
5251breq2d 4386 . . . . . . . . . . . . . . . 16
5352biimpd 207 . . . . . . . . . . . . . . 15
5449, 53sylbid 215 . . . . . . . . . . . . . 14
5547, 48, 54mp2an 672 . . . . . . . . . . . . 13
5645nn0red 10722 . . . . . . . . . . . . . . 15
5744, 56ax-mp 5 . . . . . . . . . . . . . 14
58 3re 10480 . . . . . . . . . . . . . 14
5957, 58ltnei 9583 . . . . . . . . . . . . 13
6055, 59syl 16 . . . . . . . . . . . 12
6160necomd 2716 . . . . . . . . . . 11
6261adantl 466 . . . . . . . . . 10
6343, 62ax-mp 5 . . . . . . . . 9
6463a1i 11 . . . . . . . 8
65 tpeq1 4045 . . . . . . . . . . 11
66 tpidm12 4058 . . . . . . . . . . 11
6765, 66syl6req 2507 . . . . . . . . . 10
6867fveq2d 5777 . . . . . . . . 9
6968neeq1d 2722 . . . . . . . 8
7064, 69syl5ib 219 . . . . . . 7
7142, 70sylbi 195 . . . . . 6
72 hashprlei 12263 . . . . . . . . . 10
73 prfi 7671 . . . . . . . . . . . . . . 15
74 hashcl 12211 . . . . . . . . . . . . . . . 16
7574nn0zd 10830 . . . . . . . . . . . . . . 15
7673, 75ax-mp 5 . . . . . . . . . . . . . 14
77 zleltp1 10780 . . . . . . . . . . . . . . 15
7850a1i 11 . . . . . . . . . . . . . . . . 17
7978breq2d 4386 . . . . . . . . . . . . . . . 16
8079biimpd 207 . . . . . . . . . . . . . . 15
8177, 80sylbid 215 . . . . . . . . . . . . . 14
8276, 48, 81mp2an 672 . . . . . . . . . . . . 13
8374nn0red 10722 . . . . . . . . . . . . . . 15
8473, 83ax-mp 5 . . . . . . . . . . . . . 14
8584, 58ltnei 9583 . . . . . . . . . . . . 13
8682, 85syl 16 . . . . . . . . . . . 12
8786necomd 2716 . . . . . . . . . . 11
8887adantl 466 . . . . . . . . . 10
8972, 88ax-mp 5 . . . . . . . . 9
9089a1i 11 . . . . . . . 8
91 tpeq2 4046 . . . . . . . . . . 11
92 tpidm23 4060 . . . . . . . . . . 11
9391, 92syl6req 2507 . . . . . . . . . 10
9493fveq2d 5777 . . . . . . . . 9
9594neeq1d 2722 . . . . . . . 8
9690, 95syl5ib 219 . . . . . . 7
976, 96sylbi 195 . . . . . 6
98 hashprlei 12263 . . . . . . . . . 10
99 hashcl 12211 . . . . . . . . . . . . . . . 16
10099nn0zd 10830 . . . . . . . . . . . . . . 15
1012, 100ax-mp 5 . . . . . . . . . . . . . 14
102 zleltp1 10780 . . . . . . . . . . . . . . 15
10350a1i 11 . . . . . . . . . . . . . . . . 17
104103breq2d 4386 . . . . . . . . . . . . . . . 16
105104biimpd 207 . . . . . . . . . . . . . . 15
106102, 105sylbid 215 . . . . . . . . . . . . . 14
107101, 48, 106mp2an 672 . . . . . . . . . . . . 13
10899nn0red 10722 . . . . . . . . . . . . . . 15
1092, 108ax-mp 5 . . . . . . . . . . . . . 14
110109, 58ltnei 9583 . . . . . . . . . . . . 13
111107, 110syl 16 . . . . . . . . . . . 12
112111necomd 2716 . . . . . . . . . . 11
113112adantl 466 . . . . . . . . . 10
11498, 113ax-mp 5 . . . . . . . . 9
115114a1i 11 . . . . . . . 8
116 tpeq3 4047 . . . . . . . . . . 11
117 tpidm13 4059 . . . . . . . . . . 11
118116, 117syl6req 2507 . . . . . . . . . 10
119118fveq2d 5777 . . . . . . . . 9
120119neeq1d 2722 . . . . . . . 8
121115, 120syl5ib 219 . . . . . . 7
12210, 121sylbi 195 . . . . . 6
12371, 97, 1223jaoi 1282 . . . . 5
12422, 123sylbi 195 . . . 4
125124com12 31 . . 3
126125necon4bd 2667 . 2
12741, 126impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/w3o 964  /\w3a 965  =wceq 1370  e.wcel 1757  =/=wne 2641   cvv 3052  u.cun 3408  {csn 3959  {cpr 3961  {ctp 3963   class class class wbr 4374  `cfv 5500  (class class class)co 6174   cfn 7394   cr 9366  1c1 9368   caddc 9370   clt 9503   cle 9504  2c2 10456  3c3 10457   cz 10731   chash 12188
This theorem is referenced by:  hashge3el3dif  12273  constr3lem2  23651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-oadd 7008  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-card 8194  df-cda 8422  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-nn 10408  df-2 10465  df-3 10466  df-n0 10665  df-z 10732  df-uz 10947  df-fz 11523  df-hash 12189
  Copyright terms: Public domain W3C validator