4cycl4v4e - Metamath Proof Explorer

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

Theorem 4cycl4v4e 25394

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 25360	. . . . 5 Cycles Walks
2		wlkbprop 25251	. . . . 5 Walks $/\$ $/\$ $/\$ $/\$
3	1, 2	syl 17	. . . 4 Cycles $/\$ $/\$ $/\$ $/\$
4		iscycl 25353	. . . . . 6 $/\$ $/\$ $/\$ Cycles Paths $/\$
5		ispth 25298	. . . . . . . 8 $/\$ $/\$ $/\$ Paths Trails $/\$ ..^ $/\$ ..^
6		istrl 25267	. . . . . . . . . 10 $/\$ $/\$ $/\$ Trails Word $/\$ $/\$ $/\$ ..^
7		fzo0to42pr 12000	. . . . . . . . . . . . . . . . . . 19 ..^
8	7	raleqi 2991	. . . . . . . . . . . . . . . . . 18 ..^
9		ralunb 3615	. . . . . . . . . . . . . . . . . 18 $/\$
10		2wlklem 25294	. . . . . . . . . . . . . . . . . . 19 $/\$
11		2z 10969	. . . . . . . . . . . . . . . . . . . 20
12		3z 10970	. . . . . . . . . . . . . . . . . . . 20
13		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . 23
14	13	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . 22
15		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . 23
16		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . 25
17		2p1e3 10733	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	16, 17	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 23
20	15, 19	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . 22
21	14, 20	eqeq12d 2466	. . . . . . . . . . . . . . . . . . . . 21
22		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . 23
23	22	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . 22
24		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . 23
25		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . 25
26		3p1e4 10735	. . . . . . . . . . . . . . . . . . . . . . . . 25
27	25, 26	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . 24
28	27	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 23
29	24, 28	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . 22
30	23, 29	eqeq12d 2466	. . . . . . . . . . . . . . . . . . . . 21
31	21, 30	ralprg 4021	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
32	11, 12, 31	mp2an 678	. . . . . . . . . . . . . . . . . . 19 $/\$
33	10, 32	anbi12i 703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
34	8, 9, 33	3bitri 275	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ $/\$
35		preq2 4052	. . . . . . . . . . . . . . . . . . . . . . . 24
36	35	eqcoms 2459	. . . . . . . . . . . . . . . . . . . . . . 23
37	36	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . 22
38	37	anbi2d 710	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
39	38	anbi2d 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		4pos 10705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
41		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
42	40, 41	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
43		0nn0 10884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
44	42, 43	jctil 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
45		nvnencycllem 25371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$ $/\$
46	44, 45	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$
47		1lt4 10781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
48		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
49	47, 48	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50		1nn0 10885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
51	49, 50	jctil 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
52		nvnencycllem 25371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$ $/\$
53	51, 52	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$
54	46, 53	anim12d 566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ $/\$
55		2lt4 10780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
56		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
57	55, 56	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
58		2nn0 10886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	57, 58	jctil 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
60		nvnencycllem 25371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$ $/\$
61	59, 60	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$
62		3lt4 10779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
64	62, 63	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
65		3nn0 10887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
66	64, 65	jctil 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
67		nvnencycllem 25371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word $/\$ $/\$
68	66, 67	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ Word $/\$
69	61, 68	anim12d 566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ $/\$
70	54, 69	anim12d 566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantlrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	imp 431	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		4z 10971	. . . . . . . . . . . . . . . . . . . . . . . . . 26
74		3re 10683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
75		4re 10686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
76	74, 75, 62	ltleii 9757	. . . . . . . . . . . . . . . . . . . . . . . . . 26
77		eluz2 11165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	12, 73, 76, 77	mpbir3an 1190	. . . . . . . . . . . . . . . . . . . . . . . . 25
79		4fvwrd4 11909	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
80	78, 79	mpan 676	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
81		preq12 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
82	81	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
83	82	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
84		simplr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
86	84, 85	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
87	86	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
88	83, 87	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
89		preq12 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
90	89	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
91	90	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
92		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
93		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
94	92, 93	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
95	94	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
96	91, 95	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
97	88, 96	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	biimpcd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	98	reximdv 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	reximdv 2861	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	reximdv 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	reximdv 2861	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	72, 80, 102	syl2im 39	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	exp41 615	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	104	com14 91	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
106	105	com35 93	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
107	39, 106	syl6bi 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
108	107	com12 32	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
109	108	com24 90	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
110	34, 109	sylbi 199	. . . . . . . . . . . . . . . 16 ..^ Word $/\$ $/\$ $/\$ $/\$
111	110	com13 83	. . . . . . . . . . . . . . 15 Word $/\$ ..^ $/\$ $/\$ $/\$
112	111	3imp 1202	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
113	112	com14 91	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
114		fveq2 5865	. . . . . . . . . . . . . 14
115	114	eqeq2d 2461	. . . . . . . . . . . . 13
116		oveq2 6298	. . . . . . . . . . . . . . . . 17
117	116	feq2d 5715	. . . . . . . . . . . . . . . 16
118		oveq2 6298	. . . . . . . . . . . . . . . . 17 ..^ ..^
119	118	raleqdv 2993	. . . . . . . . . . . . . . . 16 ..^ ..^
120	117, 119	3anbi23d 1342	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ $/\$ ..^ Word $/\$ $/\$ $/\$ ..^
121	120	imbi1d 319	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
122	121	imbi2d 318	. . . . . . . . . . . . 13 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
123	113, 115, 122	3imtr4d 272	. . . . . . . . . . . 12 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
124	123	com14 91	. . . . . . . . . . 11 Word $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
125	124	2a1d 27	. . . . . . . . . 10 Word $/\$ $/\$ $/\$ ..^ ..^ ..^ $/\$ $/\$ $/\$
126	6, 125	syl6bi 232	. . . . . . . . 9 $/\$ $/\$ $/\$ Trails ..^ ..^ $/\$ $/\$ $/\$
127	126	3impd 1223	. . . . . . . 8 $/\$ $/\$ $/\$ Trails $/\$ ..^ $/\$ ..^ $/\$ $/\$ $/\$
128	5, 127	sylbid 219	. . . . . . 7 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$
129	128	impd 433	. . . . . 6 $/\$ $/\$ $/\$ Paths $/\$ $/\$ $/\$ $/\$
130	4, 129	sylbid 219	. . . . 5 $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
131	130	3adant1 1026	. . . 4 $/\$ $/\$ $/\$ $/\$ Cycles $/\$ $/\$ $/\$
132	3, 131	mpcom 37	. . 3 Cycles $/\$ $/\$ $/\$
133	132	com12 32	. 2 Cycles $/\$ $/\$ $/\$
134	133	3imp 1202	1 $/\$ Cycles $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wrex 2738

cvv 3045

cun 3402

cin 3403

c0 3731

cpr 3970 class class class wbr 4402

ccnv 4833

cdm 4834

crn 4835

cres 4836

cima 4837

wfun 5576

wf 5578

cfv 5582 (class class class)co 6290

cc0 9539

c1 9540

caddc 9542

clt 9675

cle 9676

c2 10659

c3 10660

c4 10661

cn0 10869

cz 10937

cuz 11159

cfz 11784 ..^cfzo 11915

chash 12515 Word cword 12656 Walks cwalk 25226 Trails ctrail 25227 Paths cpath 25228 Cycles ccycl 25235

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-fzo 11916 df-hash 12516 df-word 12664 df-wlk 25236 df-trail 25237 df-pth 25238 df-cycl 25241

This theorem is referenced by: (None)

W3C validator