clwwlkext2edg - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > clwwlkext2edg		Unicode version

Theorem clwwlkext2edg 16272

Description: If a word concatenated with a vertex represents a closed walk (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)

**Hypotheses**
Ref	Expression
clwwlkext2edg.v	Vtx
clwwlkext2edg.e	Edg

**Assertion**
Ref	Expression
clwwlkext2edg	Word $/\$ $/\$ $/\$ ++ ClWWalksN lastS $/\$

Proof of Theorem clwwlkext2edg Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		clwwlknnn 16262	. . 3 ++ ClWWalksN
2		clwwlkext2edg.v	. . . . 5 Vtx
3		clwwlkext2edg.e	. . . . 5 Edg
4	2, 3	isclwwlknx 16266	. . . 4 ++ ClWWalksN ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++
5		ige2m2fzo 10442	. . . . . . . . . . . . . . 15 ..^
6	5	3ad2ant3 1046	. . . . . . . . . . . . . 14 Word $/\$ $/\$ ..^
7	6	adantr 276	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ..^
8		oveq1 6024	. . . . . . . . . . . . . . . 16 ♯ ++ ♯ ++
9	8	oveq2d 6033	. . . . . . . . . . . . . . 15 ♯ ++ ..^♯ ++ ..^
10	9	eleq2d 2301	. . . . . . . . . . . . . 14 ♯ ++ ..^♯ ++ ..^
11	10	adantl 277	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++ ..^
12	7, 11	mpbird 167	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++
13		fveq2 5639	. . . . . . . . . . . . . . 15 ++ ++
14		fvoveq1 6040	. . . . . . . . . . . . . . 15 ++ ++
15	13, 14	preq12d 3756	. . . . . . . . . . . . . 14 ++ ++ ++ ++
16	15	eleq1d 2300	. . . . . . . . . . . . 13 ++ ++ ++ ++
17	16	rspcv 2906	. . . . . . . . . . . 12 ..^♯ ++ ..^♯ ++ ++ ++ ++ ++
18	12, 17	syl 14	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++ ++ ++ ++ ++
19		wrdlenccats1lenm1g 11212	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ ♯ ++ ♯
20	19	eqcomd 2237	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ ♯ ♯ ++
21	20, 8	sylan9eq 2284	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ ♯ ++ ♯
22	21	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ ♯ ++ ♯
23	22	3adant3 1043	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ ♯ ++ ♯
24		eluzelcn 9766	. . . . . . . . . . . . . . . . . . . . . 22
25		1cnd 8194	. . . . . . . . . . . . . . . . . . . . . 22
26	24, 25, 25	subsub4d 8520	. . . . . . . . . . . . . . . . . . . . 21
27		1p1e2 9259	. . . . . . . . . . . . . . . . . . . . . . 23
28	27	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22
29	28	oveq2d 6033	. . . . . . . . . . . . . . . . . . . . 21
30	26, 29	eqtr2d 2265	. . . . . . . . . . . . . . . . . . . 20
31	30	3ad2ant3 1046	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$
32		oveq1 6024	. . . . . . . . . . . . . . . . . . . 20 ♯ ♯
33	32	eqcomd 2237	. . . . . . . . . . . . . . . . . . 19 ♯ ♯
34	31, 33	sylan9eq 2284	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ $/\$ ♯ ♯
35	34	ex 115	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ ♯ ♯
36	23, 35	syld 45	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ ♯ ++ ♯
37	36	imp 124	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ++ ♯
38	37	fveq2d 5643	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ ♯
39		simpl1 1026	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ♯ Word
40		s1cl 11197	. . . . . . . . . . . . . . . . . . . . 21 Word
41	40	3ad2ant2 1045	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word
42	41	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ♯ Word
43		eluz2 9760	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
44		zre 9482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45		1red 8193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
46		2re 9212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
47	46	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
48		simpl 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
49		1lt2 9312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
50	49	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
51		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
52	45, 47, 48, 50, 51	ltletrd 8602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
53		1red 8193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54		id 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
55	53, 54	posdifd 8711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
56	55	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
57	52, 56	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
58	57	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
59	44, 58	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	59	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . 25
61	60	3imp 1219	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
62	43, 61	sylbi 121	. . . . . . . . . . . . . . . . . . . . . . 23
63	62	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ ♯
64		breq2 4092	. . . . . . . . . . . . . . . . . . . . . . 23 ♯ ♯
65	64	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ ♯ ♯
66	63, 65	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ ♯ ♯
67		wrdfin 11131	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
68		fihashneq0 11055	. . . . . . . . . . . . . . . . . . . . . . . 24 ♯
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 Word ♯
70	69	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ ♯
71	70	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ ♯ ♯
72	66, 71	mpbid 147	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ ♯
73	72	3adantl2 1180	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ♯
74	39, 42, 73	3jca 1203	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ $/\$ ♯ Word $/\$ Word $/\$
75	74	ex 115	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ ♯ Word $/\$ Word $/\$
76	23, 75	syld 45	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ ♯ ++ Word $/\$ Word $/\$
77	76	imp 124	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ++ Word $/\$ Word $/\$
78		ccatval1lsw 11180	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ ++ ♯ lastS
79	77, 78	syl 14	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ♯ lastS
80	38, 79	eqtrd 2264	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ++ lastS
81		2m1e1 9260	. . . . . . . . . . . . . . . . . . . . . . 23
82	81	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22
83	82	eqcomd 2237	. . . . . . . . . . . . . . . . . . . . 21
84	83	oveq2d 6033	. . . . . . . . . . . . . . . . . . . 20
85		2cnd 9215	. . . . . . . . . . . . . . . . . . . . 21
86	24, 85, 25	subsubd 8517	. . . . . . . . . . . . . . . . . . . 20
87	84, 86	eqtr2d 2265	. . . . . . . . . . . . . . . . . . 19
88	87	3ad2ant3 1046	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$
89		eqeq2 2241	. . . . . . . . . . . . . . . . . 18 ♯ ♯
90	88, 89	syl5ibrcom 157	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ ♯ ♯
91	23, 90	syld 45	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ ♯ ++ ♯
92	91	imp 124	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ++ ♯
93	92	fveq2d 5643	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ ♯
94		id 19	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$
95	94	3adant3 1043	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ Word $/\$
96	95	adantr 276	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ++ Word $/\$
97		ccatws1ls 11218	. . . . . . . . . . . . . . 15 Word $/\$ ++ ♯
98	96, 97	syl 14	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ♯
99	93, 98	eqtrd 2264	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ++
100	80, 99	preq12d 3756	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ lastS
101	100	eleq1d 2300	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ lastS
102	18, 101	sylibd 149	. . . . . . . . . 10 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++ ++ ++ lastS
103	102	ex 115	. . . . . . . . 9 Word $/\$ $/\$ ♯ ++ ..^♯ ++ ++ ++ lastS
104	103	com13 80	. . . . . . . 8 ..^♯ ++ ++ ++ ♯ ++ Word $/\$ $/\$ lastS
105	104	3ad2ant2 1045	. . . . . . 7 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ ♯ ++ Word $/\$ $/\$ lastS
106	105	imp31 256	. . . . . 6 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++ $/\$ Word $/\$ $/\$ lastS
107	95	adantr 276	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ Word $/\$
108		lswccats1 11219	. . . . . . . . . . . . . . 15 Word $/\$ lastS ++
109	107, 108	syl 14	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ lastS ++
110	62	3ad2ant3 1046	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$
111	110	adantr 276	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ♯
112	64	adantl 277	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ♯ ♯
113	111, 112	mpbird 167	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ♯
114		ccatfv0 11179	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ ♯ ++
115	39, 42, 113, 114	syl3anc 1273	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++
116	109, 115	preq12d 3756	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ lastS ++ ++
117	116	ex 115	. . . . . . . . . . . 12 Word $/\$ $/\$ ♯ lastS ++ ++
118	23, 117	syld 45	. . . . . . . . . . 11 Word $/\$ $/\$ ♯ ++ lastS ++ ++
119	118	impcom 125	. . . . . . . . . 10 ♯ ++ $/\$ Word $/\$ $/\$ lastS ++ ++
120	119	eleq1d 2300	. . . . . . . . 9 ♯ ++ $/\$ Word $/\$ $/\$ lastS ++ ++
121	120	biimpcd 159	. . . . . . . 8 lastS ++ ++ ♯ ++ $/\$ Word $/\$ $/\$
122	121	3ad2ant3 1046	. . . . . . 7 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ ♯ ++ $/\$ Word $/\$ $/\$
123	122	impl 380	. . . . . 6 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++ $/\$ Word $/\$ $/\$
124	106, 123	jca 306	. . . . 5 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++ $/\$ Word $/\$ $/\$ lastS $/\$
125	124	ex 115	. . . 4 ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++ Word $/\$ $/\$ lastS $/\$
126	4, 125	biimtrdi 163	. . 3 ++ ClWWalksN Word $/\$ $/\$ lastS $/\$
127	1, 126	mpcom 36	. 2 ++ ClWWalksN Word $/\$ $/\$ lastS $/\$
128	127	impcom 125	1 Word $/\$ $/\$ $/\$ ++ ClWWalksN lastS $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1004

wceq 1397

wcel 2202

wne 2402

wral 2510

c0 3494

cpr 3670 class class class wbr 4088

cfv 5326 (class class class)co 6017

cfn 6908

cr 8030

cc0 8031

c1 8032

caddc 8034

clt 8213

cle 8214

cmin 8349

cn 9142

c2 9193

cz 9478

cuz 9754 ..^cfzo 10376 ♯chash 11036 Word cword 11112 lastSclsw 11157 ++ cconcat 11166

cs1 11191 Vtxcvtx 15862 Edgcedg 15907 ClWWalksN cclwwlkn 16253

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-frec 6556 df-1o 6581 df-er 6701 df-map 6818 df-en 6909 df-dom 6910 df-fin 6911 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-inn 9143 df-2 9201 df-n0 9402 df-z 9479 df-uz 9755 df-fz 10243 df-fzo 10377 df-ihash 11037 df-word 11113 df-lsw 11158 df-concat 11167 df-s1 11192 df-ndx 13084 df-slot 13085 df-base 13087 df-vtx 15864 df-clwwlk 16242 df-clwwlkn 16254

This theorem is referenced by: (None)

W3C validator