4cycl4v4e - Metamath Proof Explorer

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

Theorem 4cycl4v4e 23703

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 23669	. . . . 5 Cycles Walks
2		wlkbprop 23584	. . . . 5 Walks $/\$ $/\$ $/\$ $/\$
3	1, 2	syl 16	. . . 4 Cycles $/\$ $/\$ $/\$ $/\$
4		iscycl 23662	. . . . . 6 $/\$ $/\$ $/\$ Cycles Paths $/\$
5		ispth 23618	. . . . . . . 8 $/\$ $/\$ $/\$ Paths Trails $/\$ ..^ $/\$ ..^
6		istrl 23587	. . . . . . . . . 10 $/\$ $/\$ $/\$ Trails Word $/\$ $/\$ $/\$ ..^
7		fzo0to42pr 11732	. . . . . . . . . . . . . . . . . . . 20 ..^
8	7	raleqi 3025	. . . . . . . . . . . . . . . . . . 19 ..^
9		ralunb 3644	. . . . . . . . . . . . . . . . . . 19 $/\$
10		0z 10767	. . . . . . . . . . . . . . . . . . . . 21
11		1z 10786	. . . . . . . . . . . . . . . . . . . . 21
12		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
13	12	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . 23
14		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
15		oveq1 6206	. . . . . . . . . . . . . . . . . . . . . . . . . 26
16		0p1e1 10543	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	15, 16	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . . 24
19	14, 18	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . 23
20	13, 19	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . 22
21		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
22	21	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . 23
23		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
24		oveq1 6206	. . . . . . . . . . . . . . . . . . . . . . . . . 26
25		1p1e2 10545	. . . . . . . . . . . . . . . . . . . . . . . . . 26
26	24, 25	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25
27	26	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . . 24
28	23, 27	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . 22
30	20, 29	ralprg 4032	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
31	10, 11, 30	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $/\$
32		2z 10788	. . . . . . . . . . . . . . . . . . . . 21
33		3z 10789	. . . . . . . . . . . . . . . . . . . . 21
34		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
35	34	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . 23
36		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
37		oveq1 6206	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38		2p1e3 10555	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	37, 38	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	39	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . . 24
41	36, 40	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . 23
42	35, 41	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . 22
43		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
44	43	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . 23
45		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . 24
46		oveq1 6206	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		3p1e4 10557	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48	46, 47	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	48	fveq2d 5802	. . . . . . . . . . . . . . . . . . . . . . . 24
50	45, 49	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . 23
51	44, 50	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . 22
52	42, 51	ralprg 4032	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
53	32, 33, 52	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	31, 53	anbi12i 697	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
55	8, 9, 54	3bitri 271	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$
56		preq2 4062	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . 23
59	58	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
60	59	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		4pos 10527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62		breq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63	61, 62	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
64		0nn0 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
65	63, 64	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
66		nvnencycllem 23680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
67	65, 66	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
68		1lt4 10603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
69		breq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70	68, 69	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
71		1nn0 10705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72	70, 71	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
73		nvnencycllem 23680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
74	72, 73	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
75	67, 74	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
76		2lt4 10602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
77		breq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
78	76, 77	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
79		2nn0 10706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80	78, 79	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
81		nvnencycllem 23680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
82	80, 81	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
83		3lt4 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
84		breq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
85	83, 84	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
86		3nn0 10707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
87	85, 86	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
88		nvnencycllem 23680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95	94	nn0zi 10781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96		3re 10505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97		4re 10508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
98	96, 97, 83	ltleii 9607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
99		eluz2 10977	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
100	33, 95, 98, 99	mpbir3an 1170	. . . . . . . . . . . . . . . . . . . . . . . . . 26
101		4fvwrd4 11649	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
102	100, 101	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
103		preq12 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
104	103	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
105	104	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
106		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
107		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
108	106, 107	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
109	108	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
110	105, 109	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
111		preq12 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
112	111	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
113	112	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
114		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
115		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
116	114, 115	preq12d 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
117	116	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
118	113, 117	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
119	110, 118	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120	119	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	120	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	121	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	122	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . 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 1182	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
135	134	com14 88	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
136		fveq2 5798	. . . . . . . . . . . . . . 15
137	136	eqeq2d 2468	. . . . . . . . . . . . . 14
138		oveq2 6207	. . . . . . . . . . . . . . . . . 18
139	138	feq2d 5654	. . . . . . . . . . . . . . . . 17
140		oveq2 6207	. . . . . . . . . . . . . . . . . 18 ..^ ..^
141	140	raleqdv 3027	. . . . . . . . . . . . . . . . 17 ..^ ..^
142	139, 141	3anbi23d 1293	. . . . . . . . . . . . . . . 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 1202	. . . . . . . 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 1006	. . . 4 $/\$ $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
155	3, 154	mpcom 36	. . 3 Cycles $/\$ $/\$ $/\$
156	155	com12 31	. 2 Cycles $/\$ $/\$ $/\$
157	156	3imp 1182	1 $/\$ Cycles $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wral 2798

wrex 2799

cvv 3076

cun 3433

cin 3434

c0 3744

cpr 3986 class class class wbr 4399

ccnv 4946

cdm 4947

crn 4948

cres 4949

cima 4950

wfun 5519

wf 5521

cfv 5525 (class class class)co 6199

cc0 9392

c1 9393

caddc 9395

clt 9528

cle 9529

c2 10481

c3 10482

c4 10483

cn0 10689

cz 10756

cuz 10971

cfz 11553 ..^cfzo 11664

chash 12219 Word cword 12338 Walks cwalk 23556 Trails ctrail 23557 Paths cpath 23558 Cycles ccycl 23565

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-oadd 7033 df-er 7210 df-map 7325 df-pm 7326 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-card 8219 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-nn 10433 df-2 10490 df-3 10491 df-4 10492 df-n0 10690 df-z 10757 df-uz 10972 df-fz 11554 df-fzo 11665 df-hash 12220 df-word 12346 df-wlk 23566 df-trail 23567 df-pth 23568 df-cycl 23571

This theorem is referenced by: (None)

W3C validator