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

Theorem clwlkfoclwwlk 25572
 Description: There is an onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 30-Jun-2018.)
Hypotheses
Ref Expression
clwlkfclwwlk.1
clwlkfclwwlk.2
clwlkfclwwlk.c ClWalks
clwlkfclwwlk.f substr
Assertion
Ref Expression
clwlkfoclwwlk USGrph ClWWalksN
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem clwlkfoclwwlk
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clwlkfclwwlk.1 . . 3
2 clwlkfclwwlk.2 . . 3
3 clwlkfclwwlk.c . . 3 ClWalks
4 clwlkfclwwlk.f . . 3 substr
51, 2, 3, 4clwlkfclwwlk 25571 . 2 USGrph ClWWalksN
6 clwwlknprop 25499 . . . . 5 ClWWalksN Word
76adantl 467 . . . 4 USGrph ClWWalksN Word
8 simpl 458 . . . . . . . . . . . 12
98anim2i 571 . . . . . . . . . . 11
10 df-3an 984 . . . . . . . . . . 11
119, 10sylibr 215 . . . . . . . . . 10
12113adant2 1024 . . . . . . . . 9 Word
1312adantl 467 . . . . . . . 8 USGrph Word
14 isclwwlkn 25496 . . . . . . . 8 ClWWalksN ClWWalks
1513, 14syl 17 . . . . . . 7 USGrph Word ClWWalksN ClWWalks
16 simpl1 1008 . . . . . . . . . 10 USGrph Word USGrph
17 simpr2 1012 . . . . . . . . . 10 USGrph Word Word
18 eleq1 2495 . . . . . . . . . . . . . . . 16
19 prmnn 14625 . . . . . . . . . . . . . . . . 17
2019nnge1d 10660 . . . . . . . . . . . . . . . 16
2118, 20syl6bir 232 . . . . . . . . . . . . . . 15
2221adantl 467 . . . . . . . . . . . . . 14
23223ad2ant3 1028 . . . . . . . . . . . . 13 Word
2423com12 32 . . . . . . . . . . . 12 Word
25243ad2ant3 1028 . . . . . . . . . . 11 USGrph Word
2625imp 430 . . . . . . . . . 10 USGrph Word
27 clwlkisclwwlk2 25517 . . . . . . . . . 10 USGrph Word ClWalks ++ ClWWalks
2816, 17, 26, 27syl3anc 1264 . . . . . . . . 9 USGrph Word ClWalks ++ ClWWalks
2928bicomd 204 . . . . . . . 8 USGrph Word ClWWalks ClWalks ++
3029anbi1d 709 . . . . . . 7 USGrph Word ClWWalks ClWalks ++
3115, 30bitrd 256 . . . . . 6 USGrph Word ClWWalksN ClWalks ++
32 df-br 4424 . . . . . . . . . . 11 ClWalks ++ ++ ClWalks
33 simpl 458 . . . . . . . . . . . . . . 15 ++ ClWalks USGrph Word ++ ClWalks
34 prmnn 14625 . . . . . . . . . . . . . . . . . . . . . . . 24
3534nnge1d 10660 . . . . . . . . . . . . . . . . . . . . . . 23
36353ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . 22 USGrph
3736adantr 466 . . . . . . . . . . . . . . . . . . . . 21 USGrph Word
38 breq2 4427 . . . . . . . . . . . . . . . . . . . . . . . 24
3938adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23
40393ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . 22 Word
4140adantl 467 . . . . . . . . . . . . . . . . . . . . 21 USGrph Word
4237, 41mpbird 235 . . . . . . . . . . . . . . . . . . . 20 USGrph Word
4317, 42jca 534 . . . . . . . . . . . . . . . . . . 19 USGrph Word Word
4443adantr 466 . . . . . . . . . . . . . . . . . 18 USGrph Word Word
45 clwlkswlks 25485 . . . . . . . . . . . . . . . . . 18 ++ ClWalks ++ Walks
46 wlklenvclwlk 25566 . . . . . . . . . . . . . . . . . 18 Word ++ Walks
4744, 45, 46syl2im 39 . . . . . . . . . . . . . . . . 17 USGrph Word ++ ClWalks
4847impcom 431 . . . . . . . . . . . . . . . 16 ++ ClWalks USGrph Word
49 vex 3083 . . . . . . . . . . . . . . . . . . . 20
50 ovex 6334 . . . . . . . . . . . . . . . . . . . 20 ++
5149, 50op1st 6816 . . . . . . . . . . . . . . . . . . 19 ++
5251a1i 11 . . . . . . . . . . . . . . . . . 18 USGrph Word ++
5352fveq2d 5886 . . . . . . . . . . . . . . . . 17 USGrph Word ++
5453ad2antrl 732 . . . . . . . . . . . . . . . 16 ++ ClWalks USGrph Word ++
55 eqcom 2431 . . . . . . . . . . . . . . . . . 18
5655biimpi 197 . . . . . . . . . . . . . . . . 17
5756ad2antll 733 . . . . . . . . . . . . . . . 16 ++ ClWalks USGrph Word
5848, 54, 573eqtr4d 2473 . . . . . . . . . . . . . . 15 ++ ClWalks USGrph Word ++
591fveq2i 5885 . . . . . . . . . . . . . . . . . 18
6059eqeq1i 2429 . . . . . . . . . . . . . . . . 17
61 fveq2 5882 . . . . . . . . . . . . . . . . . . 19 ++ ++
6261fveq2d 5886 . . . . . . . . . . . . . . . . . 18 ++ ++
6362eqeq1d 2424 . . . . . . . . . . . . . . . . 17 ++ ++
6460, 63syl5bb 260 . . . . . . . . . . . . . . . 16 ++ ++
6564, 3elrab2 3230 . . . . . . . . . . . . . . 15 ++ ++ ClWalks ++
6633, 58, 65sylanbrc 668 . . . . . . . . . . . . . 14 ++ ClWalks USGrph Word ++
6743, 45, 46syl2im 39 . . . . . . . . . . . . . . . . . . . . . 22 USGrph Word ++ ClWalks
6867ad2antrl 732 . . . . . . . . . . . . . . . . . . . . 21 ++ ClWalks USGrph Word ++ ClWalks
6968imp 430 . . . . . . . . . . . . . . . . . . . 20 ++ ClWalks USGrph Word ++ ClWalks
7069opeq2d 4194 . . . . . . . . . . . . . . . . . . 19 ++ ClWalks USGrph Word ++ ClWalks
7170oveq2d 6322 . . . . . . . . . . . . . . . . . 18 ++ ClWalks USGrph Word ++ ClWalks ++ substr ++ substr
72 simpr 462 . . . . . . . . . . . . . . . . . . . 20 ++ ClWalks USGrph Word ++ ClWalks ++ ClWalks
73 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . . . . 25
7473eqcoms 2434 . . . . . . . . . . . . . . . . . . . . . . . 24
7574imbi2d 317 . . . . . . . . . . . . . . . . . . . . . . 23 ++ ClWalks ++ ClWalks
7675ad2antll 733 . . . . . . . . . . . . . . . . . . . . . 22 ++ ClWalks USGrph Word ++ ClWalks ++ ClWalks
7768, 76mpbird 235 . . . . . . . . . . . . . . . . . . . . 21 ++ ClWalks USGrph Word ++ ClWalks
7877imp 430 . . . . . . . . . . . . . . . . . . . 20 ++ ClWalks USGrph Word ++ ClWalks
7951a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ++ ++
8079fveq2d 5886 . . . . . . . . . . . . . . . . . . . . . . . 24 ++ ++
8162, 80eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . 23 ++
8281eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . 22 ++
8360, 82syl5bb 260 . . . . . . . . . . . . . . . . . . . . 21 ++
8483, 3elrab2 3230 . . . . . . . . . . . . . . . . . . . 20 ++ ++ ClWalks
8572, 78, 84sylanbrc 668 . . . . . . . . . . . . . . . . . . 19 ++ ClWalks USGrph Word ++ ClWalks ++
86 ovex 6334 . . . . . . . . . . . . . . . . . . 19 ++ substr
8759opeq2i 4191 . . . . . . . . . . . . . . . . . . . . . 22
882, 87oveq12i 6318 . . . . . . . . . . . . . . . . . . . . 21 substr substr
89 fveq2 5882 . . . . . . . . . . . . . . . . . . . . . . 23 ++ ++
9062opeq2d 4194 . . . . . . . . . . . . . . . . . . . . . . 23 ++ ++
9189, 90oveq12d 6324 . . . . . . . . . . . . . . . . . . . . . 22 ++ substr ++ substr ++
9249, 50op2nd 6817 . . . . . . . . . . . . . . . . . . . . . . 23 ++ ++
9351fveq2i 5885 . . . . . . . . . . . . . . . . . . . . . . . 24 ++
9493opeq2i 4191 . . . . . . . . . . . . . . . . . . . . . . 23 ++
9592, 94oveq12i 6318 . . . . . . . . . . . . . . . . . . . . . 22 ++ substr ++ ++ substr
9691, 95syl6eq 2479 . . . . . . . . . . . . . . . . . . . . 21 ++ substr ++ substr
9788, 96syl5eq 2475 . . . . . . . . . . . . . . . . . . . 20 ++ substr ++ substr
9897, 4fvmptg 5963 . . . . . . . . . . . . . . . . . . 19 ++ ++ substr ++ ++ substr
9985, 86, 98sylancl 666 . . . . . . . . . . . . . . . . . 18 ++ ClWalks USGrph Word ++ ClWalks ++ ++ substr
10043ad2antrl 732 . . . . . . . . . . . . . . . . . . . 20 ++ ClWalks USGrph Word Word
101100adantr 466 . . . . . . . . . . . . . . . . . . 19 ++ ClWalks USGrph Word ++ ClWalks Word
102 simpl 458 . . . . . . . . . . . . . . . . . . . . 21 Word Word
103 wrdsymb1 12709 . . . . . . . . . . . . . . . . . . . . . 22 Word
104103s1cld 12747 . . . . . . . . . . . . . . . . . . . . 21 Word Word
105 eqidd 2423 . . . . . . . . . . . . . . . . . . . . 21 Word
106 swrdccatid 12856 . . . . . . . . . . . . . . . . . . . . 21 Word Word ++ substr
107102, 104, 105, 106syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20 Word ++ substr
108107eqcomd 2430 . . . . . . . . . . . . . . . . . . 19 Word ++ substr
109101, 108syl 17 . . . . . . . . . . . . . . . . . 18 ++ ClWalks USGrph Word ++ ClWalks ++ substr
11071, 99, 1093eqtr4rd 2474 . . . . . . . . . . . . . . . . 17 ++ ClWalks USGrph Word ++ ClWalks ++
111110ex 435 . . . . . . . . . . . . . . . 16 ++ ClWalks USGrph Word ++ ClWalks ++
112111adantr 466 . . . . . . . . . . . . . . 15 ++ ClWalks USGrph Word ++ ++ ClWalks ++
113 fveq2 5882 . . . . . . . . . . . . . . . . . 18 ++ ++
114113eqeq2d 2436 . . . . . . . . . . . . . . . . 17 ++ ++
115114imbi2d 317 . . . . . . . . . . . . . . . 16 ++ ++ ClWalks ++ ClWalks ++
116115adantl 467 . . . . . . . . . . . . . . 15 ++ ClWalks USGrph Word ++ ++ ClWalks ++ ClWalks ++
117112, 116mpbird 235 . . . . . . . . . . . . . 14 ++ ClWalks USGrph Word ++ ++ ClWalks
11866, 117rspcimedv 3184 . . . . . . . . . . . . 13 ++ ClWalks USGrph Word ++ ClWalks
119118ex 435 . . . . . . . . . . . 12 ++ ClWalks USGrph Word ++ ClWalks
120119pm2.43b 52 . . . . . . . . . . 11 USGrph Word ++ ClWalks
12132, 120syl5bi 220 . . . . . . . . . 10 USGrph Word ClWalks ++
122121exlimdv 1772 . . . . . . . . 9 USGrph Word ClWalks ++
123122ex 435 . . . . . . . 8 USGrph Word ClWalks ++
124123com23 81 . . . . . . 7 USGrph Word ClWalks ++
125124impd 432 . . . . . 6 USGrph Word ClWalks ++
12631, 125sylbid 218 . . . . 5 USGrph Word ClWWalksN
127126impancom 441 . . . 4 USGrph ClWWalksN Word
1287, 127mpd 15 . . 3 USGrph ClWWalksN
129128ralrimiva 2836 . 2 USGrph ClWWalksN
130 dffo3 6053 . 2 ClWWalksN ClWWalksN ClWWalksN
1315, 129, 130sylanbrc 668 1 USGrph ClWWalksN
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872  wral 2771  wrex 2772  crab 2775  cvv 3080  cop 4004   class class class wbr 4423   cmpt 4482  wf 5597  wfo 5599  cfv 5601  (class class class)co 6306  c1st 6806  c2nd 6807  cfn 7581  cc0 9547  c1 9548   cle 9684  cn0 10877  chash 12522  Word cword 12661   ++ cconcat 12663  cs1 12664   substr csubstr 12665  cprime 14622   USGrph cusg 25056   Walks cwalk 25225   ClWalks cclwlk 25474   ClWWalks cclwwlk 25475   ClWWalksN cclwwlkn 25476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-2o 7195  df-oadd 7198  df-er 7375  df-map 7486  df-pm 7487  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-card 8382  df-cda 8606  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-2 10676  df-n0 10878  df-z 10946  df-uz 11168  df-rp 11311  df-fz 11793  df-fzo 11924  df-hash 12523  df-word 12669  df-lsw 12670  df-concat 12671  df-s1 12672  df-substr 12673  df-dvds 14306  df-prm 14623  df-usgra 25059  df-wlk 25235  df-clwlk 25477  df-clwwlk 25478  df-clwwlkn 25479 This theorem is referenced by:  clwlkf1oclwwlk  25578
 Copyright terms: Public domain W3C validator