4cycl4v4e - Metamath Proof Explorer

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

Theorem 4cycl4v4e 24793

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 24759	. . . . 5 Cycles Walks
2		wlkbprop 24650	. . . . 5 Walks $/\$ $/\$ $/\$ $/\$
3	1, 2	syl 16	. . . 4 Cycles $/\$ $/\$ $/\$ $/\$
4		iscycl 24752	. . . . . 6 $/\$ $/\$ $/\$ Cycles Paths $/\$
5		ispth 24697	. . . . . . . 8 $/\$ $/\$ $/\$ Paths Trails $/\$ ..^ $/\$ ..^
6		istrl 24666	. . . . . . . . . 10 $/\$ $/\$ $/\$ Trails Word $/\$ $/\$ $/\$ ..^
7		fzo0to42pr 11904	. . . . . . . . . . . . . . . . . . . 20 ..^
8	7	raleqi 3058	. . . . . . . . . . . . . . . . . . 19 ..^
9		ralunb 3681	. . . . . . . . . . . . . . . . . . 19 $/\$
10		2wlklem 24693	. . . . . . . . . . . . . . . . . . . 20 $/\$
11		2z 10917	. . . . . . . . . . . . . . . . . . . . 21
12		3z 10918	. . . . . . . . . . . . . . . . . . . . 21
13		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
14	13	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23
15		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
16		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17		2p1e3 10680	. . . . . . . . . . . . . . . . . . . . . . . . . 26
18	16, 17	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . . . 25
19	18	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24
20	15, 19	preq12d 4119	. . . . . . . . . . . . . . . . . . . . . . 23
21	14, 20	eqeq12d 2479	. . . . . . . . . . . . . . . . . . . . . 22
22		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
23	22	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23
24		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
25		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . . . 26
26		3p1e4 10682	. . . . . . . . . . . . . . . . . . . . . . . . . 26
27	25, 26	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . . . 25
28	27	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24
29	24, 28	preq12d 4119	. . . . . . . . . . . . . . . . . . . . . . 23
30	23, 29	eqeq12d 2479	. . . . . . . . . . . . . . . . . . . . . 22
31	21, 30	ralprg 4081	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
32	11, 12, 31	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $/\$
33	10, 32	anbi12i 697	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
34	8, 9, 33	3bitri 271	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ $/\$
35		preq2 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	35	eqcoms 2469	. . . . . . . . . . . . . . . . . . . . . . . 24
37	36	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . 23
38	37	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
39	38	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		4pos 10652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
41		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
42	40, 41	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
43		0nn0 10831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
44	42, 43	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
45		nvnencycllem 24770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
46	44, 45	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
47		1lt4 10728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
49	47, 48	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
50		1nn0 10832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
51	49, 50	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
52		nvnencycllem 24770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
53	51, 52	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
54	46, 53	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
55		2lt4 10727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
56		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
57	55, 56	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
58		2nn0 10833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
59	57, 58	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
60		nvnencycllem 24770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
61	59, 60	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
62		3lt4 10726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
64	62, 63	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
65		3nn0 10834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
66	64, 65	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
67		nvnencycllem 24770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ Word $/\$ $/\$
68	66, 67	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$
69	61, 68	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$ $/\$ $/\$
70	54, 69	anim12d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantlrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		4z 10919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
74		3re 10630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
75		4re 10633	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	74, 75, 62	ltleii 9724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
77		eluz2 11112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	12, 73, 76, 77	mpbir3an 1178	. . . . . . . . . . . . . . . . . . . . . . . . . 26
79		4fvwrd4 11819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
80	78, 79	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
81		preq12 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
82	81	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
83	82	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
84		simplr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
85		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
86	84, 85	preq12d 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
87	86	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
88	83, 87	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
89		preq12 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
90	89	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
91	90	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
92		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
93		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
94	92, 93	preq12d 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
95	94	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
96	91, 95	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
97	88, 96	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	98	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	reximdv 2931	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	72, 80, 102	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	exp41 610	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	104	com14 88	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
106	105	com35 90	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
107	39, 106	syl6bi 228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
108	107	com12 31	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
109	108	com24 87	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
110	34, 109	sylbi 195	. . . . . . . . . . . . . . . . 17 ..^ Word $/\$ $/\$ $/\$ $/\$
111	110	com13 80	. . . . . . . . . . . . . . . 16 Word $/\$ ..^ $/\$ $/\$ $/\$
112	111	3imp 1190	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
113	112	com14 88	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
114		fveq2 5872	. . . . . . . . . . . . . . 15
115	114	eqeq2d 2471	. . . . . . . . . . . . . 14
116		oveq2 6304	. . . . . . . . . . . . . . . . . 18
117	116	feq2d 5724	. . . . . . . . . . . . . . . . 17
118		oveq2 6304	. . . . . . . . . . . . . . . . . 18 ..^ ..^
119	118	raleqdv 3060	. . . . . . . . . . . . . . . . 17 ..^ ..^
120	117, 119	3anbi23d 1302	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ..^ Word $/\$ $/\$ $/\$ ..^
121	120	imbi1d 317	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
122	121	imbi2d 316	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
123	113, 115, 122	3imtr4d 268	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
124	123	com14 88	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
125	124	a1d 25	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$
126	125	a1d 25	. . . . . . . . . 10 Word $/\$ $/\$ $/\$ ..^ ..^ ..^ $/\$ $/\$ $/\$
127	6, 126	syl6bi 228	. . . . . . . . 9 $/\$ $/\$ $/\$ Trails ..^ ..^ $/\$ $/\$ $/\$
128	127	3impd 1210	. . . . . . . 8 $/\$ $/\$ $/\$ Trails $/\$ ..^ $/\$ ..^ $/\$ $/\$ $/\$
129	5, 128	sylbid 215	. . . . . . 7 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$
130	129	impd 431	. . . . . 6 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$ $/\$
131	4, 130	sylbid 215	. . . . 5 $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
132	131	3adant1 1014	. . . 4 $/\$ $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
133	3, 132	mpcom 36	. . 3 Cycles $/\$ $/\$ $/\$
134	133	com12 31	. 2 Cycles $/\$ $/\$ $/\$
135	134	3imp 1190	1 $/\$ Cycles $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1395

wcel 1819

wral 2807

wrex 2808

cvv 3109

cun 3469

cin 3470

c0 3793

cpr 4034 class class class wbr 4456

ccnv 5007

cdm 5008

crn 5009

cres 5010

cima 5011

wfun 5588

wf 5590

cfv 5594 (class class class)co 6296

cc0 9509

c1 9510

caddc 9512

clt 9645

cle 9646

c2 10606

c3 10607

c4 10608

cn0 10816

cz 10885

cuz 11106

cfz 11697 ..^cfzo 11821

chash 12408 Word cword 12538 Walks cwalk 24625 Trails ctrail 24626 Paths cpath 24627 Cycles ccycl 24634

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-n0 10817 df-z 10886 df-uz 11107 df-fz 11698 df-fzo 11822 df-hash 12409 df-word 12546 df-wlk 24635 df-trail 24636 df-pth 24637 df-cycl 24640

This theorem is referenced by: (None)

W3C validator