clwwlkext2edg - Intuitionistic Logic Explorer

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

Theorem clwwlkext2edg 16300

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 16290	. . 3 ++ ClWWalksN
2		clwwlkext2edg.v	. . . . 5 Vtx
3		clwwlkext2edg.e	. . . . 5 Edg
4	2, 3	isclwwlknx 16294	. . . 4 ++ ClWWalksN ++ Word $/\$ ..^♯ ++ ++ ++ $/\$ lastS ++ ++ $/\$ ♯ ++
5		ige2m2fzo 10447	. . . . . . . . . . . . . . 15 ..^
6	5	3ad2ant3 1046	. . . . . . . . . . . . . 14 Word $/\$ $/\$ ..^
7	6	adantr 276	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ..^
8		oveq1 6028	. . . . . . . . . . . . . . . 16 ♯ ++ ♯ ++
9	8	oveq2d 6037	. . . . . . . . . . . . . . 15 ♯ ++ ..^♯ ++ ..^
10	9	eleq2d 2301	. . . . . . . . . . . . . 14 ♯ ++ ..^♯ ++ ..^
11	10	adantl 277	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++ ..^
12	7, 11	mpbird 167	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ♯ ++ ..^♯ ++
13		fveq2 5640	. . . . . . . . . . . . . . 15 ++ ++
14		fvoveq1 6044	. . . . . . . . . . . . . . 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 11220	. . . . . . . . . . . . . . . . . . . . 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 9770	. . . . . . . . . . . . . . . . . . . . . 22
25		1cnd 8198	. . . . . . . . . . . . . . . . . . . . . 22
26	24, 25, 25	subsub4d 8524	. . . . . . . . . . . . . . . . . . . . 21
27		1p1e2 9263	. . . . . . . . . . . . . . . . . . . . . . 23
28	27	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22
29	28	oveq2d 6037	. . . . . . . . . . . . . . . . . . . . 21
30	26, 29	eqtr2d 2265	. . . . . . . . . . . . . . . . . . . 20
31	30	3ad2ant3 1046	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$
32		oveq1 6028	. . . . . . . . . . . . . . . . . . . 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 5644	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ ♯
39		simpl1 1026	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ♯ Word
40		s1cl 11205	. . . . . . . . . . . . . . . . . . . . 21 Word
41	40	3ad2ant2 1045	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word
42	41	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ♯ Word
43		eluz2 9764	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
44		zre 9486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45		1red 8197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
46		2re 9216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
47	46	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
48		simpl 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
49		1lt2 9316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
50	49	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
51		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
52	45, 47, 48, 50, 51	ltletrd 8606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
53		1red 8197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54		id 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
55	53, 54	posdifd 8715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11139	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
68		fihashneq0 11060	. . . . . . . . . . . . . . . . . . . . . . . 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 11188	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ ++ ♯ lastS
79	77, 78	syl 14	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ♯ lastS
80	38, 79	eqtrd 2264	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ♯ ++ ++ lastS
81		2m1e1 9264	. . . . . . . . . . . . . . . . . . . . . . 23
82	81	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22
83	82	eqcomd 2237	. . . . . . . . . . . . . . . . . . . . 21
84	83	oveq2d 6037	. . . . . . . . . . . . . . . . . . . 20
85		2cnd 9219	. . . . . . . . . . . . . . . . . . . . 21
86	24, 85, 25	subsubd 8521	. . . . . . . . . . . . . . . . . . . 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 5644	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ♯ ++ ++ ++ ♯
94		id 19	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$
95	94	3adant3 1043	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ Word $/\$
96	95	adantr 276	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ♯ ++ Word $/\$
97		ccatws1ls 11226	. . . . . . . . . . . . . . 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 11227	. . . . . . . . . . . . . . 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 11187	. . . . . . . . . . . . . . 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 6021

cfn 6912

cr 8034

cc0 8035

c1 8036

caddc 8038

clt 8217

cle 8218

cmin 8353

cn 9146

c2 9197

cz 9482

cuz 9758 ..^cfzo 10380 ♯chash 11041 Word cword 11120 lastSclsw 11165 ++ cconcat 11174

cs1 11199 Vtxcvtx 15890 Edgcedg 15935 ClWWalksN cclwwlkn 16281

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 8126 ax-resscn 8127 ax-1cn 8128 ax-1re 8129 ax-icn 8130 ax-addcl 8131 ax-addrcl 8132 ax-mulcl 8133 ax-mulrcl 8134 ax-addcom 8135 ax-mulcom 8136 ax-addass 8137 ax-mulass 8138 ax-distr 8139 ax-i2m1 8140 ax-0lt1 8141 ax-1rid 8142 ax-0id 8143 ax-rnegex 8144 ax-precex 8145 ax-cnre 8146 ax-pre-ltirr 8147 ax-pre-ltwlin 8148 ax-pre-lttrn 8149 ax-pre-apti 8150 ax-pre-ltadd 8151 ax-pre-mulgt0 8152

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 5974 df-ov 6024 df-oprab 6025 df-mpo 6026 df-1st 6306 df-2nd 6307 df-recs 6474 df-frec 6560 df-1o 6585 df-er 6705 df-map 6822 df-en 6913 df-dom 6914 df-fin 6915 df-pnf 8219 df-mnf 8220 df-xr 8221 df-ltxr 8222 df-le 8223 df-sub 8355 df-neg 8356 df-reap 8758 df-ap 8765 df-inn 9147 df-2 9205 df-n0 9406 df-z 9483 df-uz 9759 df-fz 10247 df-fzo 10381 df-ihash 11042 df-word 11121 df-lsw 11166 df-concat 11175 df-s1 11200 df-ndx 13106 df-slot 13107 df-base 13109 df-vtx 15892 df-clwwlk 16270 df-clwwlkn 16282

This theorem is referenced by: (None)

W3C validator