Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  numclwlk2lem2f1o Structured version   Unicode version

Theorem numclwlk2lem2f1o 30623
 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 2501 . . . . . . . . 9
2 fveq2 5688 . . . . . . . . . 10
3 oveq1 6097 . . . . . . . . . 10 substr substr
42, 3eqeq12d 2455 . . . . . . . . 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 30622 . . . . . . 7 substr
146, 13chvarv 1963 . . . . . 6 substr
15143adant1 1001 . . . . 5 FriendGrph substr
1615imp 429 . . . 4 FriendGrph substr
177, 8, 9, 10, 11, 12numclwlk2lem2f 30621 . . . . 5 FriendGrph
1817ffvelrnda 5840 . . . 4 FriendGrph
1916, 18eqeltrrd 2516 . . 3 FriendGrph substr
2019ralrimiva 2797 . 2 FriendGrph substr
217, 8, 9, 10, 11numclwwlk2lem1 30620 . . . . 5 FriendGrph concat
2221imp 429 . . . 4 FriendGrph concat
23 nnnn0 10582 . . . . . . . . . 10
247, 8, 9, 10numclwwlkovq 30617 . . . . . . . . . 10 WWalksN lastS
2523, 24sylan2 471 . . . . . . . . 9 WWalksN lastS
2625eleq2d 2508 . . . . . . . 8 WWalksN lastS
27263adant1 1001 . . . . . . 7 FriendGrph WWalksN lastS
28 fveq1 5687 . . . . . . . . . 10
2928eqeq1d 2449 . . . . . . . . 9
30 fveq2 5688 . . . . . . . . . 10 lastS lastS
3130neeq1d 2619 . . . . . . . . 9 lastS lastS
3229, 31anbi12d 705 . . . . . . . 8 lastS lastS
3332elrab 3114 . . . . . . 7 WWalksN lastS WWalksN lastS
3427, 33syl6bb 261 . . . . . 6 FriendGrph WWalksN lastS
35 wwlknimpb 30263 . . . . . . . . . . . . . 14 WWalksN Word
36 simpll 748 . . . . . . . . . . . . . . . 16 Word FriendGrph Word
37 2nn0 10592 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
3923, 38nn0addcld 10636 . . . . . . . . . . . . . . . . . . . . . . 23
407, 8, 9, 10, 11numclwwlkovh 30619 . . . . . . . . . . . . . . . . . . . . . . 23
4139, 40sylan2 471 . . . . . . . . . . . . . . . . . . . . . 22
4241eleq2d 2508 . . . . . . . . . . . . . . . . . . . . 21
43 fveq1 5687 . . . . . . . . . . . . . . . . . . . . . . . . 25
4443eqeq1d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24
45 fveq1 5687 . . . . . . . . . . . . . . . . . . . . . . . . 25
4645, 43neeq12d 2621 . . . . . . . . . . . . . . . . . . . . . . . 24
4744, 46anbi12d 705 . . . . . . . . . . . . . . . . . . . . . . 23
4847elrab 3114 . . . . . . . . . . . . . . . . . . . . . 22
4948a1i 11 . . . . . . . . . . . . . . . . . . . . 21
507numclwwlkfvc 30595 . . . . . . . . . . . . . . . . . . . . . . . . 25 ClWWalksN
5139, 50syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 ClWWalksN
5251eleq2d 2508 . . . . . . . . . . . . . . . . . . . . . . 23 ClWWalksN
5352adantl 463 . . . . . . . . . . . . . . . . . . . . . 22 ClWWalksN
5453anbi1d 699 . . . . . . . . . . . . . . . . . . . . 21 ClWWalksN
5542, 49, 543bitrd 279 . . . . . . . . . . . . . . . . . . . 20 ClWWalksN
56553adant1 1001 . . . . . . . . . . . . . . . . . . 19 FriendGrph ClWWalksN
5756adantl 463 . . . . . . . . . . . . . . . . . 18 Word FriendGrph ClWWalksN
58 clwwlknprop 30360 . . . . . . . . . . . . . . . . . . . . 21 ClWWalksN Word
59 lencl 12245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word
60 simprr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word Word
61 df-2 10376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6362oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
64 nncn 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
65 ax-1cn 9336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6665a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6764, 66, 66addassd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6863, 67eqtr4d 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6968adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7069eqeq2d 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7170biimpcd 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7271adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Word
7372impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word
74 oveq1 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7574ad3antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word
7673, 75eqtr4d 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word
7760, 76jca 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word Word
7877exp31 601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word Word
7959, 78sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word Word Word
8079com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word Word Word
81803ad2ant3 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 FriendGrph Word Word Word
8281impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word FriendGrph Word Word
8382com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word Word FriendGrph Word
8483ex 434 . . . . . . . . . . . . . . . . . . . . . . . 24 Word Word FriendGrph Word
8584adantl 463 . . . . . . . . . . . . . . . . . . . . . . 23 Word Word FriendGrph Word
8685impcom 430 . . . . . . . . . . . . . . . . . . . . . 22 Word Word FriendGrph Word
87863adant1 1001 . . . . . . . . . . . . . . . . . . . . 21 Word Word FriendGrph Word
8858, 87syl 16 . . . . . . . . . . . . . . . . . . . 20 ClWWalksN Word FriendGrph Word
8988adantr 462 . . . . . . . . . . . . . . . . . . 19 ClWWalksN Word FriendGrph Word
9089com12 31 . . . . . . . . . . . . . . . . . 18 Word FriendGrph ClWWalksN Word
9157, 90sylbid 215 . . . . . . . . . . . . . . . . 17 Word FriendGrph Word
9291ralrimiv 2796 . . . . . . . . . . . . . . . 16 Word FriendGrph Word
9336, 92jca 529 . . . . . . . . . . . . . . 15 Word FriendGrph Word Word
9493ex 434 . . . . . . . . . . . . . 14 Word FriendGrph Word Word
9535, 94syl 16 . . . . . . . . . . . . 13 WWalksN FriendGrph Word Word
9695adantr 462 . . . . . . . . . . . 12 WWalksN lastS FriendGrph Word Word
9796imp 429 . . . . . . . . . . 11 WWalksN lastS FriendGrph Word Word
98 reuccats1 30186 . . . . . . . . . . 11 Word Word concat substr
9997, 98syl 16 . . . . . . . . . 10 WWalksN lastS FriendGrph concat substr
10099imp 429 . . . . . . . . 9 WWalksN lastS FriendGrph concat substr
101 simpr 458 . . . . . . . . . . . . . . . 16 Word
102101eqcomd 2446 . . . . . . . . . . . . . . 15 Word
10335, 102syl 16 . . . . . . . . . . . . . 14 WWalksN
104103ad4antr 726 . . . . . . . . . . . . 13 WWalksN lastS FriendGrph concat
105104opeq2d 4063 . . . . . . . . . . . 12 WWalksN lastS FriendGrph concat
106105oveq2d 6106 . . . . . . . . . . 11 WWalksN lastS FriendGrph concat substr substr
107106eqeq2d 2452 . . . . . . . . . 10 WWalksN lastS FriendGrph concat substr substr
108107reubidva 2902 . . . . . . . . 9 WWalksN lastS FriendGrph concat substr substr
109100, 108mpbird 232 . . . . . . . 8 WWalksN lastS FriendGrph concat substr
110109exp31 601 . . . . . . 7 WWalksN lastS FriendGrph concat substr
111110com12 31 . . . . . 6 FriendGrph WWalksN lastS concat substr
11234, 111sylbid 215 . . . . 5 FriendGrph concat substr
113112imp 429 . . . 4 FriendGrph concat substr
11422, 113mpd 15 . . 3 FriendGrph substr
115114ralrimiva 2797 . 2 FriendGrph substr
11612f1ompt 5862 . 2 substr substr
11720, 115, 116sylanbrc 659 1 FriendGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 960   wceq 1364   wcel 1761   wne 2604  wral 2713  wreu 2715  crab 2717  cvv 2970  cop 3880   class class class wbr 4289   cmpt 4347  wf1o 5414  cfv 5415  (class class class)co 6090   cmpt2 6092  cc 9276  cc0 9278  c1 9279   caddc 9281   cmin 9591  cn 10318  c2 10367  cn0 10575  cuz 10857  chash 12099  Word cword 12217   lastS clsw 12218   concat cconcat 12219  cs1 12220   substr csubstr 12221   WWalksN cwwlkn 30237   ClWWalksN cclwwlkn 30339   FriendGrph cfrgra 30505 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-map 7212  df-pm 7213  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-2 10376  df-n0 10576  df-z 10643  df-uz 10858  df-fz 11434  df-fzo 11545  df-hash 12100  df-word 12225  df-lsw 12226  df-concat 12227  df-s1 12228  df-substr 12229  df-wwlk 30238  df-wwlkn 30239  df-clwwlk 30341  df-clwwlkn 30342  df-frgra 30506 This theorem is referenced by:  numclwwlk2lem3  30624
 Copyright terms: Public domain W3C validator