4cycl4v4e - Metamath Proof Explorer

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

Theorem 4cycl4v4e 24339

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 24305	. . . . 5 Cycles Walks
2		wlkbprop 24196	. . . . 5 Walks $/\$ $/\$ $/\$ $/\$
3	1, 2	syl 16	. . . 4 Cycles $/\$ $/\$ $/\$ $/\$
4		iscycl 24298	. . . . . 6 $/\$ $/\$ $/\$ Cycles Paths $/\$
5		ispth 24243	. . . . . . . 8 $/\$ $/\$ $/\$ Paths Trails $/\$ ..^ $/\$ ..^
6		istrl 24212	. . . . . . . . . 10 $/\$ $/\$ $/\$ Trails Word $/\$ $/\$ $/\$ ..^
7		fzo0to42pr 11865	. . . . . . . . . . . . . . . . . . . 20 ..^
8	7	raleqi 3062	. . . . . . . . . . . . . . . . . . 19 ..^
9		ralunb 3685	. . . . . . . . . . . . . . . . . . 19 $/\$
10		0z 10871	. . . . . . . . . . . . . . . . . . . . 21
11		1z 10890	. . . . . . . . . . . . . . . . . . . . 21
12		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
13	12	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . 23
14		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
15		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . . . . 26
16		0p1e1 10643	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	15, 16	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . . 24
19	14, 18	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . 23
20	13, 19	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . 22
21		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
22	21	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . 23
23		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
24		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . . . . 26
25		1p1e2 10645	. . . . . . . . . . . . . . . . . . . . . . . . . 26
26	24, 25	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . 25
27	26	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . . 24
28	23, 27	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . 22
30	20, 29	ralprg 4076	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
31	10, 11, 30	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $/\$
32		2z 10892	. . . . . . . . . . . . . . . . . . . . 21
33		3z 10893	. . . . . . . . . . . . . . . . . . . . 21
34		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
35	34	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . 23
36		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
37		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38		2p1e3 10655	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	37, 38	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	39	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . . 24
41	36, 40	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . 23
42	35, 41	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . 22
43		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
44	43	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . 23
45		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
46		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		3p1e4 10657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48	46, 47	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	48	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . . 24
50	45, 49	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . 23
51	44, 50	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . 22
52	42, 51	ralprg 4076	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
53	32, 33, 52	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	31, 53	anbi12i 697	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
55	8, 9, 54	3bitri 271	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$
56		preq2 4107	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcoms 2479	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . 23
59	58	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
60	59	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		4pos 10627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63	61, 62	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
64		0nn0 10806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
65	63, 64	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
66		nvnencycllem 24316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
67	65, 66	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
68		1lt4 10703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
69		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70	68, 69	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
71		1nn0 10807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72	70, 71	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
73		nvnencycllem 24316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
74	72, 73	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
75	67, 74	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
76		2lt4 10702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
77		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
78	76, 77	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
79		2nn0 10808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80	78, 79	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
81		nvnencycllem 24316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
82	80, 81	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
83		3lt4 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
84		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
85	83, 84	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
86		3nn0 10809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
87	85, 86	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
88		nvnencycllem 24316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
89	87, 88	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
90	82, 89	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
91	75, 90	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantlrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	92	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		4nn0 10810	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95	94	nn0zi 10885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96		3re 10605	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97		4re 10608	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
98	96, 97, 83	ltleii 9703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
99		eluz2 11084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
100	33, 95, 98, 99	mpbir3an 1178	. . . . . . . . . . . . . . . . . . . . . . . . . 26
101		4fvwrd4 11786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
102	100, 101	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
103		preq12 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
104	103	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
105	104	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
106		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
107		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
108	106, 107	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
109	108	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
110	105, 109	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
111		preq12 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
112	111	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
113	112	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
114		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
115		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
116	114, 115	preq12d 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
117	116	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
118	113, 117	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
119	110, 118	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120	119	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	120	reximdv 2937	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	121	reximdv 2937	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	122	reximdv 2937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	reximdv 2937	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	93, 102, 124	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	125	exp41 610	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	com14 88	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
128	127	com35 90	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
129	60, 128	syl6bi 228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
130	129	com12 31	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
131	130	com24 87	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
132	55, 131	sylbi 195	. . . . . . . . . . . . . . . . 17 ..^ Word $/\$ $/\$ $/\$ $/\$
133	132	com13 80	. . . . . . . . . . . . . . . 16 Word $/\$ ..^ $/\$ $/\$ $/\$
134	133	3imp 1190	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
135	134	com14 88	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
136		fveq2 5864	. . . . . . . . . . . . . . 15
137	136	eqeq2d 2481	. . . . . . . . . . . . . 14
138		oveq2 6290	. . . . . . . . . . . . . . . . . 18
139	138	feq2d 5716	. . . . . . . . . . . . . . . . 17
140		oveq2 6290	. . . . . . . . . . . . . . . . . 18 ..^ ..^
141	140	raleqdv 3064	. . . . . . . . . . . . . . . . 17 ..^ ..^
142	139, 141	3anbi23d 1302	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ..^ Word $/\$ $/\$ $/\$ ..^
143	142	imbi1d 317	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
144	143	imbi2d 316	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
145	135, 137, 144	3imtr4d 268	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
146	145	com14 88	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
147	146	a1d 25	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
148	147	a1d 25	. . . . . . . . . 10 Word $/\$ $/\$ $/\$ ..^ ..^ ..^ $/\$ $/\$ $/\$
149	6, 148	syl6bi 228	. . . . . . . . 9 $/\$ $/\$ $/\$ Trails ..^ ..^ $/\$ $/\$ $/\$
150	149	3impd 1210	. . . . . . . 8 $/\$ $/\$ $/\$ Trails $/\$ ..^ $/\$ ..^ $/\$ $/\$ $/\$
151	5, 150	sylbid 215	. . . . . . 7 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$
152	151	impd 431	. . . . . 6 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$ $/\$
153	4, 152	sylbid 215	. . . . 5 $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
154	153	3adant1 1014	. . . 4 $/\$ $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
155	3, 154	mpcom 36	. . 3 Cycles $/\$ $/\$ $/\$
156	155	com12 31	. 2 Cycles $/\$ $/\$ $/\$
157	156	3imp 1190	1 $/\$ Cycles $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

wral 2814

wrex 2815

cvv 3113

cun 3474

cin 3475

c0 3785

cpr 4029 class class class wbr 4447

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

wfun 5580

wf 5582

cfv 5586 (class class class)co 6282

cc0 9488

c1 9489

caddc 9491

clt 9624

cle 9625

c2 10581

c3 10582

c4 10583

cn0 10791

cz 10860

cuz 11078

cfz 11668 ..^cfzo 11788

chash 12367 Word cword 12494 Walks cwalk 24171 Trails ctrail 24172 Paths cpath 24173 Cycles ccycl 24180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-card 8316 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-n0 10792 df-z 10861 df-uz 11079 df-fz 11669 df-fzo 11789 df-hash 12368 df-word 12502 df-wlk 24181 df-trail 24182 df-pth 24183 df-cycl 24186

This theorem is referenced by: (None)

W3C validator