numclwlk1lem2foa - Metamath Proof Explorer

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

Theorem numclwlk1lem2foa 25296

Description: Going forth and back form the end of a (closed) walk. (Contributed by Alexander van der Vekens, 22-Sep-2018.)

**Hypotheses**
Ref	Expression
numclwwlk.c	ClWWalksN
numclwwlk.f
numclwwlk.g	$/\$

**Assertion**
Ref	Expression
numclwlk1lem2foa	USGrph $/\$ $/\$ $/\$ Neighbors ++ ++

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem numclwlk1lem2foa Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 994	. . . . . . . . . 10 USGrph $/\$ $/\$ USGrph
2		uzuzle23 11122	. . . . . . . . . . . 12
3		uznn0sub 11113	. . . . . . . . . . . 12
4	2, 3	syl 16	. . . . . . . . . . 11
5	4	3ad2ant3 1017	. . . . . . . . . 10 USGrph $/\$ $/\$
6		simp2 995	. . . . . . . . . 10 USGrph $/\$ $/\$
7		numclwwlk.c	. . . . . . . . . . 11 ClWWalksN
8		numclwwlk.f	. . . . . . . . . . 11
9	7, 8	numclwwlkovfel2 25288	. . . . . . . . . 10 USGrph $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$
10	1, 5, 6, 9	syl3anc 1226	. . . . . . . . 9 USGrph $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$
11		simplll 757	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ USGrph $/\$ $/\$
12		simpr 459	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors Neighbors
13	12	adantr 463	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ Neighbors
14		simpr 459	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$
15	7, 8	numclwwlkovf2ex 25291	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++
16	11, 13, 14, 15	syl3anc 1226	. . . . . . . . . . . . . . . 16 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++
17		nbgraisvtx 24636	. . . . . . . . . . . . . . . . . . . . . . . 24 USGrph Neighbors
18	17	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . 23 USGrph $/\$ $/\$ Neighbors
19	18	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors
20		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ Word
21		s1cl 12606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word
22	21	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 USGrph $/\$ $/\$ Word
23	22	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ $/\$ USGrph $/\$ $/\$ Word
24	23	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ Word
25		s1cl 12606	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word
26	25	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ Word
27		ccatass 12597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ Word ++ ++ ++ ++
28	27	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ Word ++ ++ substr ++ ++ substr
29	20, 24, 26, 28	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
30		ccatcl 12585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word ++ Word
31	23, 25, 30	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ ++ Word
32		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word $/\$
33	32	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$
34	33	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ $/\$ USGrph $/\$ $/\$
35	34	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$
36		swrdccatid 12716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ ++ Word $/\$ ++ ++ substr
37	20, 31, 35, 36	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ ++ ++ substr
38	29, 37	eqtr2d 2496	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ $/\$ USGrph $/\$ $/\$ $/\$ ++ ++ substr
39	38	exp31 602	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ USGrph $/\$ $/\$ ++ ++ substr
40	39	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ USGrph $/\$ $/\$ ++ ++ substr
41	40	impcom 428	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ ++ ++ substr
42	19, 41	syld 44	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++ substr
43	42	imp 427	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors ++ ++ substr
44	43	eleq1d 2523	. . . . . . . . . . . . . . . . . . 19 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors ++ ++ substr
45	44	biimpd 207	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors ++ ++ substr
46	45	imp 427	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++ substr
47		simplrl 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Word $/\$
48	6	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$
49	48	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
50	47, 49	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$
51		ccatw2s1p2 12633	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ $/\$ $/\$ ++ ++
52	50, 51	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ++ ++
53		eluzelcn 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54		2cnd 10604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
55		1cnd 9601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
56		subsub 9840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
57	56	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
58	53, 54, 55, 57	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		2m1e1 10646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60	59	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
61	60	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62	58, 61	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63	62	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 USGrph $/\$ $/\$
64	63	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$
65	64	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$
66	65	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ++ ++ ++ ++
67	52, 66	eqtr3d 2497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ++ ++
68	67	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ ++ ++
69	19, 68	syld 44	. . . . . . . . . . . . . . . . . . . . . . . 24 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++
70	69	impcom 428	. . . . . . . . . . . . . . . . . . . . . . 23 Neighbors $/\$ USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ ++ ++
71	70	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . 22 Neighbors $/\$ USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++ Neighbors
72	71	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 Neighbors $/\$ USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++ Neighbors
73	72	ex 432	. . . . . . . . . . . . . . . . . . . 20 Neighbors USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++ Neighbors
74	73	pm2.43a 49	. . . . . . . . . . . . . . . . . . 19 Neighbors USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ ++ ++ Neighbors
75	74	impcom 428	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors ++ ++ Neighbors
76	75	adantr 463	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++ Neighbors
77		ccatw2s1p1 12632	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ $/\$ ++ ++
78	50, 77	syl 16	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ++ ++
79	78	ex 432	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ ++ ++
80	19, 79	syld 44	. . . . . . . . . . . . . . . . . . 19 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++
81	80	imp 427	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors ++ ++
82	81	adantr 463	. . . . . . . . . . . . . . . . 17 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++
83	46, 76, 82	3jca 1174	. . . . . . . . . . . . . . . 16 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
84	16, 83	jca 530	. . . . . . . . . . . . . . 15 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ Neighbors $/\$ ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
85	84	exp31 602	. . . . . . . . . . . . . 14 USGrph $/\$ $/\$ $/\$ Word $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
86	85	expcom 433	. . . . . . . . . . . . 13 Word $/\$ $/\$ USGrph $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
87	86	exp31 602	. . . . . . . . . . . 12 Word USGrph $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
88	87	3ad2ant1 1015	. . . . . . . . . . 11 Word $/\$ ..^ $/\$ lastS USGrph $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
89	88	3imp 1188	. . . . . . . . . 10 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ USGrph $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
90	89	com12 31	. . . . . . . . 9 USGrph $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
91	10, 90	sylbid 215	. . . . . . . 8 USGrph $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
92	91	com14 88	. . . . . . 7 Neighbors USGrph $/\$ $/\$ ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
93	92	pm2.43i 47	. . . . . 6 Neighbors USGrph $/\$ $/\$ ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
94	93	imp 427	. . . . 5 $/\$ Neighbors USGrph $/\$ $/\$ ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
95	94	impcom 428	. . . 4 USGrph $/\$ $/\$ $/\$ $/\$ Neighbors ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
96		oveq1 6277	. . . . . . 7 ++ ++ substr ++ ++ substr
97	96	eleq1d 2523	. . . . . 6 ++ ++ substr ++ ++ substr
98		fveq1 5847	. . . . . . 7 ++ ++ ++ ++
99	98	eleq1d 2523	. . . . . 6 ++ ++ Neighbors ++ ++ Neighbors
100		fveq1 5847	. . . . . . 7 ++ ++ ++ ++
101	100	eqeq1d 2456	. . . . . 6 ++ ++ ++ ++
102	97, 99, 101	3anbi123d 1297	. . . . 5 ++ ++ substr $/\$ Neighbors $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
103	102	elrab 3254	. . . 4 ++ ++ substr $/\$ Neighbors $/\$ ++ ++ $/\$ ++ ++ substr $/\$ ++ ++ Neighbors $/\$ ++ ++
104	95, 103	sylibr 212	. . 3 USGrph $/\$ $/\$ $/\$ $/\$ Neighbors ++ ++ substr $/\$ Neighbors $/\$
105		numclwwlk.g	. . . . 5 $/\$
106	7, 8, 105	extwwlkfab 25295	. . . 4 USGrph $/\$ $/\$ substr $/\$ Neighbors $/\$
107	106	adantr 463	. . 3 USGrph $/\$ $/\$ $/\$ $/\$ Neighbors substr $/\$ Neighbors $/\$
108	104, 107	eleqtrrd 2545	. 2 USGrph $/\$ $/\$ $/\$ $/\$ Neighbors ++ ++
109	108	ex 432	1 USGrph $/\$ $/\$ $/\$ Neighbors ++ ++

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wral 2804

crab 2808

cpr 4018

cop 4022 class class class wbr 4439

cmpt 4497

crn 4989

cfv 5570 (class class class)co 6270

cmpt2 6272

cc 9479

cc0 9481

c1 9482

caddc 9484

cmin 9796

c2 10581

c3 10582

cn0 10791

cuz 11082 ..^cfzo 11799

chash 12390 Word cword 12521 lastS clsw 12522 ++ cconcat 12523

cs1 12524 substr csubstr 12525 USGrph cusg 24535 Neighbors cnbgra 24622 ClWWalksN cclwwlkn 24954

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-map 7414 df-pm 7415 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-nn 10532 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11083 df-rp 11222 df-fz 11676 df-fzo 11800 df-hash 12391 df-word 12529 df-lsw 12530 df-concat 12531 df-s1 12532 df-substr 12533 df-usgra 24538 df-nbgra 24625 df-clwwlk 24956 df-clwwlkn 24957

This theorem is referenced by: numclwlk1lem2fo 25300

W3C validator