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

Theorem numclwlk2lem2f1o 24937
 Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018.)
Hypotheses
Ref Expression
numclwwlk.c ClWWalksN
numclwwlk.f
numclwwlk.g
numclwwlk.q WWalksN lastS
numclwwlk.h
numclwwlk.r substr
Assertion
Ref Expression
numclwlk2lem2f1o FriendGrph
Distinct variable groups:   ,   ,   ,   ,,   ,   ,,   ,   ,,,   ,   ,,,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,
Allowed substitution hints:   (,)   (,,,)   (,,)   (,,)   (,)

Proof of Theorem numclwlk2lem2f1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2539 . . . . . . . . 9
2 fveq2 5872 . . . . . . . . . 10
3 oveq1 6302 . . . . . . . . . 10 substr substr
42, 3eqeq12d 2489 . . . . . . . . 9 substr substr
51, 4imbi12d 320 . . . . . . . 8 substr substr
65imbi2d 316 . . . . . . 7 substr substr
7 numclwwlk.c . . . . . . . 8 ClWWalksN
8 numclwwlk.f . . . . . . . 8
9 numclwwlk.g . . . . . . . 8
10 numclwwlk.q . . . . . . . 8 WWalksN lastS
11 numclwwlk.h . . . . . . . 8
12 numclwwlk.r . . . . . . . 8 substr
137, 8, 9, 10, 11, 12numclwlk2lem2fv 24936 . . . . . . 7 substr
146, 13chvarv 1983 . . . . . 6 substr
15143adant1 1014 . . . . 5 FriendGrph substr
1615imp 429 . . . 4 FriendGrph substr
177, 8, 9, 10, 11, 12numclwlk2lem2f 24935 . . . . 5 FriendGrph
1817ffvelrnda 6032 . . . 4 FriendGrph
1916, 18eqeltrrd 2556 . . 3 FriendGrph substr
2019ralrimiva 2881 . 2 FriendGrph substr
217, 8, 9, 10, 11numclwwlk2lem1 24934 . . . . 5 FriendGrph concat
2221imp 429 . . . 4 FriendGrph concat
23 nnnn0 10814 . . . . . . . . . 10
247, 8, 9, 10numclwwlkovq 24931 . . . . . . . . . 10 WWalksN lastS
2523, 24sylan2 474 . . . . . . . . 9 WWalksN lastS
2625eleq2d 2537 . . . . . . . 8 WWalksN lastS
27263adant1 1014 . . . . . . 7 FriendGrph WWalksN lastS
28 fveq1 5871 . . . . . . . . . 10
2928eqeq1d 2469 . . . . . . . . 9
30 fveq2 5872 . . . . . . . . . 10 lastS lastS
3130neeq1d 2744 . . . . . . . . 9 lastS lastS
3229, 31anbi12d 710 . . . . . . . 8 lastS lastS
3332elrab 3266 . . . . . . 7 WWalksN lastS WWalksN lastS
3427, 33syl6bb 261 . . . . . 6 FriendGrph WWalksN lastS
35 wwlknimpb 24536 . . . . . . . . . . . . . 14 WWalksN Word
36 simpll 753 . . . . . . . . . . . . . . . 16 Word FriendGrph Word
37 2nn0 10824 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
3923, 38nn0addcld 10868 . . . . . . . . . . . . . . . . . . . . . . 23
407, 8, 9, 10, 11numclwwlkovh 24933 . . . . . . . . . . . . . . . . . . . . . . 23
4139, 40sylan2 474 . . . . . . . . . . . . . . . . . . . . . 22
4241eleq2d 2537 . . . . . . . . . . . . . . . . . . . . 21
43 fveq1 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
4443eqeq1d 2469 . . . . . . . . . . . . . . . . . . . . . . . 24
45 fveq1 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
4645, 43neeq12d 2746 . . . . . . . . . . . . . . . . . . . . . . . 24
4744, 46anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 23
4847elrab 3266 . . . . . . . . . . . . . . . . . . . . . 22
4948a1i 11 . . . . . . . . . . . . . . . . . . . . 21
507numclwwlkfvc 24909 . . . . . . . . . . . . . . . . . . . . . . . . 25 ClWWalksN
5139, 50syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 ClWWalksN
5251eleq2d 2537 . . . . . . . . . . . . . . . . . . . . . . 23 ClWWalksN
5352adantl 466 . . . . . . . . . . . . . . . . . . . . . 22 ClWWalksN
5453anbi1d 704 . . . . . . . . . . . . . . . . . . . . 21 ClWWalksN
5542, 49, 543bitrd 279 . . . . . . . . . . . . . . . . . . . 20 ClWWalksN
56553adant1 1014 . . . . . . . . . . . . . . . . . . 19 FriendGrph ClWWalksN
5756adantl 466 . . . . . . . . . . . . . . . . . 18 Word FriendGrph ClWWalksN
58 clwwlknprop 24604 . . . . . . . . . . . . . . . . . . . . 21 ClWWalksN Word
59 lencl 12542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word
60 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word Word
61 df-2 10606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6362oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
64 nncn 10556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
65 1cnd 9624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6664, 65, 65addassd 9630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6763, 66eqtr4d 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6867adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6968eqeq2d 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7069biimpcd 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7170adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Word
7271impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word
73 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7473ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word
7572, 74eqtr4d 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word
7660, 75jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word Word
7776exp31 604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word Word
7859, 77sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word Word Word
7978com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word Word Word
80793ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 FriendGrph Word Word Word
8180impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word FriendGrph Word Word
8281com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word Word FriendGrph Word
8382ex 434 . . . . . . . . . . . . . . . . . . . . . . . 24 Word Word FriendGrph Word
8483adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23 Word Word FriendGrph Word
8584impcom 430 . . . . . . . . . . . . . . . . . . . . . 22 Word Word FriendGrph Word
86853adant1 1014 . . . . . . . . . . . . . . . . . . . . 21 Word Word FriendGrph Word
8758, 86syl 16 . . . . . . . . . . . . . . . . . . . 20 ClWWalksN Word FriendGrph Word
8887adantr 465 . . . . . . . . . . . . . . . . . . 19 ClWWalksN Word FriendGrph Word
8988com12 31 . . . . . . . . . . . . . . . . . 18 Word FriendGrph ClWWalksN Word
9057, 89sylbid 215 . . . . . . . . . . . . . . . . 17 Word FriendGrph Word
9190ralrimiv 2879 . . . . . . . . . . . . . . . 16 Word FriendGrph Word
9236, 91jca 532 . . . . . . . . . . . . . . 15 Word FriendGrph Word Word
9392ex 434 . . . . . . . . . . . . . 14 Word FriendGrph Word Word
9435, 93syl 16 . . . . . . . . . . . . 13 WWalksN FriendGrph Word Word
9594adantr 465 . . . . . . . . . . . 12 WWalksN lastS FriendGrph Word Word
9695imp 429 . . . . . . . . . . 11 WWalksN lastS FriendGrph Word Word
97 reuccats1 12685 . . . . . . . . . . 11 Word Word concat substr
9896, 97syl 16 . . . . . . . . . 10 WWalksN lastS FriendGrph concat substr
9998imp 429 . . . . . . . . 9 WWalksN lastS FriendGrph concat substr
100 simpr 461 . . . . . . . . . . . . . . . 16 Word
101100eqcomd 2475 . . . . . . . . . . . . . . 15 Word
10235, 101syl 16 . . . . . . . . . . . . . 14 WWalksN
103102ad4antr 731 . . . . . . . . . . . . 13 WWalksN lastS FriendGrph concat
104103opeq2d 4226 . . . . . . . . . . . 12 WWalksN lastS FriendGrph concat
105104oveq2d 6311 . . . . . . . . . . 11 WWalksN lastS FriendGrph concat substr substr
106105eqeq2d 2481 . . . . . . . . . 10 WWalksN lastS FriendGrph concat substr substr
107106reubidva 3050 . . . . . . . . 9 WWalksN lastS FriendGrph concat substr substr
10899, 107mpbird 232 . . . . . . . 8 WWalksN lastS FriendGrph concat substr
109108exp31 604 . . . . . . 7 WWalksN lastS FriendGrph concat substr
110109com12 31 . . . . . 6 FriendGrph WWalksN lastS concat substr
11134, 110sylbid 215 . . . . 5 FriendGrph concat substr
112111imp 429 . . . 4 FriendGrph concat substr
11322, 112mpd 15 . . 3 FriendGrph substr
114113ralrimiva 2881 . 2 FriendGrph substr
11512f1ompt 6054 . 2 substr substr
11620, 114, 115sylanbrc 664 1 FriendGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767   wne 2662  wral 2817  wreu 2819  crab 2821  cvv 3118  cop 4039   class class class wbr 4453   cmpt 4511  wf1o 5593  cfv 5594  (class class class)co 6295   cmpt2 6297  cc0 9504  c1 9505   caddc 9507   cmin 9817  cn 10548  c2 10597  cn0 10807  cuz 11094  chash 12385  Word cword 12514   lastS clsw 12515   concat cconcat 12516  cs1 12517   substr csubstr 12518   WWalksN cwwlkn 24510   ClWWalksN cclwwlkn 24581   FriendGrph cfrgra 24820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-fzo 11805  df-hash 12386  df-word 12522  df-lsw 12523  df-concat 12524  df-s1 12525  df-substr 12526  df-wwlk 24511  df-wwlkn 24512  df-clwwlk 24583  df-clwwlkn 24584  df-frgra 24821 This theorem is referenced by:  numclwwlk2lem3  24938
 Copyright terms: Public domain W3C validator