4cycl4v4e - Metamath Proof Explorer

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

Theorem 4cycl4v4e 21606

Description: If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)

**Assertion**
Ref	Expression
4cycl4v4e	$/\$ Cycles $/\$ $/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem 4cycl4v4e Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cycliswlk 21572	. . . . 5 Cycles Walks
2		wlkbprop 21487	. . . . 5 Walks $/\$ $/\$ $/\$ $/\$
3	1, 2	syl 16	. . . 4 Cycles $/\$ $/\$ $/\$ $/\$
4		iscycl 21565	. . . . . 6 $/\$ $/\$ $/\$ Cycles Paths $/\$
5		ispth 21521	. . . . . . . 8 $/\$ $/\$ $/\$ Paths Trails $/\$ ..^ $/\$ ..^
6		istrl 21490	. . . . . . . . . 10 $/\$ $/\$ $/\$ Trails Word $/\$ $/\$ $/\$ ..^
7		fzo0to42pr 11141	. . . . . . . . . . . . . . . . . . . 20 ..^
8	7	raleqi 2868	. . . . . . . . . . . . . . . . . . 19 ..^
9		ralunb 3488	. . . . . . . . . . . . . . . . . . 19 $/\$
10		0z 10249	. . . . . . . . . . . . . . . . . . . . 21
11		1z 10267	. . . . . . . . . . . . . . . . . . . . 21
12		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
13	12	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . 23
14		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
15		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . 26
16		0p1e1 10049	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	15, 16	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . 24
19	14, 18	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . 23
20	13, 19	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . 22
21		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
22	21	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . 23
23		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
24		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . 26
25		1p1e2 10050	. . . . . . . . . . . . . . . . . . . . . . . . . 26
26	24, 25	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
27	26	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . 24
28	23, 27	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . 22
30	20, 29	ralprg 3817	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
31	10, 11, 30	mp2an 654	. . . . . . . . . . . . . . . . . . . 20 $/\$
32		2z 10268	. . . . . . . . . . . . . . . . . . . . 21
33		3nn0 10195	. . . . . . . . . . . . . . . . . . . . . 22
34	33	nn0zi 10262	. . . . . . . . . . . . . . . . . . . . 21
35		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
36	35	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . 23
37		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
38		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39		2p1e3 10059	. . . . . . . . . . . . . . . . . . . . . . . . . 26
40	38, 39	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . 24
42	37, 41	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . 23
43	36, 42	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . 22
44		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
45	44	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . 23
46		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24
47		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48		3p1e4 10060	. . . . . . . . . . . . . . . . . . . . . . . . . 26
49	47, 48	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
50	49	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . 24
51	46, 50	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . 23
52	45, 51	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . 22
53	43, 52	ralprg 3817	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
54	32, 34, 53	mp2an 654	. . . . . . . . . . . . . . . . . . . 20 $/\$
55	31, 54	anbi12i 679	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
56	8, 9, 55	3bitri 263	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$
57		preq2 3844	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	57	eqcoms 2407	. . . . . . . . . . . . . . . . . . . . . . . 24
59	58	eqeq2d 2415	. . . . . . . . . . . . . . . . . . . . . . 23
60	59	anbi2d 685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
61	60	anbi2d 685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		4pos 10042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
64	62, 63	mpbiri 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
65		0nn0 10192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
66	64, 65	jctil 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
67		nvnencycllem 21583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
68	66, 67	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
69		1lt4 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71	69, 70	mpbiri 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72		1nn0 10193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
73	71, 72	jctil 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
74		nvnencycllem 21583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
75	73, 74	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
76	68, 75	anim12d 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
77		2lt4 10102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
78		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
79	77, 78	mpbiri 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80		2nn0 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
81	79, 80	jctil 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
82		nvnencycllem 21583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
83	81, 82	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
84		3lt4 10101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
85		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
86	84, 85	mpbiri 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
87	86, 33	jctil 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
88		nvnencycllem 21583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
89	87, 88	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
90	83, 89	anim12d 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
91	76, 90	anim12d 547	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantlrr 702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	92	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		4nn0 10196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95	94	nn0zi 10262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96		3re 10027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97		4re 10029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
98	96, 97, 84	ltleii 9152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
99		eluz2 10450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
100	34, 95, 98, 99	mpbir3an 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26
101		4fvwrd4 11076	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
102	100, 101	mpan 652	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
103		preq12 3845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
104	103	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
105	104	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
106		simplr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
107		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
108	106, 107	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
109	108	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
110	105, 109	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
111		preq12 3845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
112	111	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
113	112	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
114		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
115		simpll 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
116	114, 115	preq12d 3851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
117	116	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
118	113, 117	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
119	110, 118	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120	119	biimpcd 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	120	reximdv 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	121	reximdv 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	122	reximdv 2777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	reximdv 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	93, 102, 124	syl2im 36	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	125	exp41 594	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	com14 84	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
128	127	com35 86	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
129	61, 128	syl6bi 220	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
130	129	com12 29	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
131	130	com24 83	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
132	56, 131	sylbi 188	. . . . . . . . . . . . . . . . 17 ..^ Word $/\$ $/\$ $/\$ $/\$
133	132	com13 76	. . . . . . . . . . . . . . . 16 Word $/\$ ..^ $/\$ $/\$ $/\$
134	133	3imp 1147	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
135	134	com14 84	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
136		fveq2 5687	. . . . . . . . . . . . . . 15
137	136	eqeq2d 2415	. . . . . . . . . . . . . 14
138		oveq2 6048	. . . . . . . . . . . . . . . . . 18
139	138	feq2d 5540	. . . . . . . . . . . . . . . . 17
140		oveq2 6048	. . . . . . . . . . . . . . . . . 18 ..^ ..^
141	140	raleqdv 2870	. . . . . . . . . . . . . . . . 17 ..^ ..^
142	139, 141	3anbi23d 1257	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ..^ Word $/\$ $/\$ $/\$ ..^
143	142	imbi1d 309	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
144	143	imbi2d 308	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
145	135, 137, 144	3imtr4d 260	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
146	145	com14 84	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
147	146	a1d 23	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
148	147	a1d 23	. . . . . . . . . 10 Word $/\$ $/\$ $/\$ ..^ ..^ ..^ $/\$ $/\$ $/\$
149	6, 148	syl6bi 220	. . . . . . . . 9 $/\$ $/\$ $/\$ Trails ..^ ..^ $/\$ $/\$ $/\$
150	149	3impd 1167	. . . . . . . 8 $/\$ $/\$ $/\$ Trails $/\$ ..^ $/\$ ..^ $/\$ $/\$ $/\$
151	5, 150	sylbid 207	. . . . . . 7 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$
152	151	imp3a 421	. . . . . 6 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$ $/\$
153	4, 152	sylbid 207	. . . . 5 $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
154	153	3adant1 975	. . . 4 $/\$ $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
155	3, 154	mpcom 34	. . 3 Cycles $/\$ $/\$ $/\$
156	155	com12 29	. 2 Cycles $/\$ $/\$ $/\$
157	156	3imp 1147	1 $/\$ Cycles $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

wrex 2667

cvv 2916

cun 3278

cin 3279

c0 3588

cpr 3775 class class class wbr 4172

ccnv 4836

cdm 4837

crn 4838

cres 4839

cima 4840

wfun 5407

wf 5409

cfv 5413 (class class class)co 6040

cc0 8946

c1 8947

caddc 8949

clt 9076

cle 9077

c2 10005

c3 10006

c4 10007

cn0 10177

cz 10238

cuz 10444

cfz 10999 ..^cfzo 11090

chash 11573 Word cword 11672 Walks cwalk 21459 Trails ctrail 21460 Paths cpath 21461 Cycles ccycl 21468

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-fzo 11091 df-hash 11574 df-word 11678 df-wlk 21469 df-trail 21470 df-pth 21471 df-cycl 21474

W3C validator