cusgr3cyclex

Description: Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023)

		Ref	Expression
	Hypothesis	cusgr3cyclex.1	$⊢ V = Vtx (G)$
	Assertion	cusgr3cyclex	$⊢ (G \in ComplUSGraph \land 2 < \|V\|) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$

Proof

Step	Hyp	Ref	Expression
1		cusgr3cyclex.1	$⊢ V = Vtx (G)$
2		3anass	$⊢ (a \in V \land b \in V \land c \in V) \leftrightarrow (a \in V \land (b \in V \land c \in V))$
3	2	bianass	$⊢ (G \in ComplUSGraph \land (a \in V \land b \in V \land c \in V)) \leftrightarrow ((G \in ComplUSGraph \land a \in V) \land (b \in V \land c \in V))$
4		cusgrusgr	$⊢ G \in ComplUSGraph \to G \in USGraph$
5		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
6	4 5	syl	$⊢ G \in ComplUSGraph \to G \in UMGraph$
7		3simpc	$⊢ (a \in V \land b \in V \land c \in V) \to (b \in V \land c \in V)$
8	7	ancli	$⊢ (a \in V \land b \in V \land c \in V) \to ((a \in V \land b \in V \land c \in V) \land (b \in V \land c \in V))$
9		df-3an	$⊢ (a \neq b \land a \neq c \land b \neq c) \leftrightarrow ((a \neq b \land a \neq c) \land b \neq c)$
10	9	biimpi	$⊢ (a \neq b \land a \neq c \land b \neq c) \to ((a \neq b \land a \neq c) \land b \neq c)$
11		an32	$⊢ (((a \in V \land b \in V \land c \in V) \land (b \in V \land c \in V)) \land (a \neq b \land a \neq c)) \leftrightarrow (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land (b \in V \land c \in V))$
12	11	anbi1i	$⊢ ((((a \in V \land b \in V \land c \in V) \land (b \in V \land c \in V)) \land (a \neq b \land a \neq c)) \land b \neq c) \leftrightarrow ((((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land (b \in V \land c \in V)) \land b \neq c)$
13		anass	$⊢ ((((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land (b \in V \land c \in V)) \land b \neq c) \leftrightarrow (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land ((b \in V \land c \in V) \land b \neq c))$
14	12 13	sylbb	$⊢ ((((a \in V \land b \in V \land c \in V) \land (b \in V \land c \in V)) \land (a \neq b \land a \neq c)) \land b \neq c) \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land ((b \in V \land c \in V) \land b \neq c))$
15	14	anasss	$⊢ (((a \in V \land b \in V \land c \in V) \land (b \in V \land c \in V)) \land ((a \neq b \land a \neq c) \land b \neq c)) \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land ((b \in V \land c \in V) \land b \neq c))$
16	8 10 15	syl2an	$⊢ ((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land ((b \in V \land c \in V) \land b \neq c))$
17		anandi3	$⊢ (a \in V \land b \in V \land c \in V) \leftrightarrow ((a \in V \land b \in V) \land (a \in V \land c \in V))$
18	17	anbi1i	$⊢ ((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \leftrightarrow (((a \in V \land b \in V) \land (a \in V \land c \in V)) \land (a \neq b \land a \neq c))$
19		an4	$⊢ (((a \in V \land b \in V) \land (a \in V \land c \in V)) \land (a \neq b \land a \neq c)) \leftrightarrow (((a \in V \land b \in V) \land a \neq b) \land ((a \in V \land c \in V) \land a \neq c))$
20	18 19	sylbb	$⊢ ((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \to (((a \in V \land b \in V) \land a \neq b) \land ((a \in V \land c \in V) \land a \neq c))$
21		df-3an	$⊢ (a \in V \land b \in V \land a \neq b) \leftrightarrow ((a \in V \land b \in V) \land a \neq b)$
22		eqid	$⊢ Edg (G) = Edg (G)$
23	1 22	cusgredgex2	$⊢ G \in ComplUSGraph \to ((a \in V \land b \in V \land a \neq b) \to \{a, b\} \in Edg (G))$
24	21 23	syl5bir	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V) \land a \neq b) \to \{a, b\} \in Edg (G))$
25		df-3an	$⊢ (a \in V \land c \in V \land a \neq c) \leftrightarrow ((a \in V \land c \in V) \land a \neq c)$
26	1 22	cusgredgex2	$⊢ G \in ComplUSGraph \to ((a \in V \land c \in V \land a \neq c) \to \{a, c\} \in Edg (G))$
27	25 26	syl5bir	$⊢ G \in ComplUSGraph \to (((a \in V \land c \in V) \land a \neq c) \to \{a, c\} \in Edg (G))$
28	24 27	anim12d	$⊢ G \in ComplUSGraph \to ((((a \in V \land b \in V) \land a \neq b) \land ((a \in V \land c \in V) \land a \neq c)) \to (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)))$
29	20 28	syl5	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \to (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)))$
30		df-3an	$⊢ (b \in V \land c \in V \land b \neq c) \leftrightarrow ((b \in V \land c \in V) \land b \neq c)$
31	1 22	cusgredgex2	$⊢ G \in ComplUSGraph \to ((b \in V \land c \in V \land b \neq c) \to \{b, c\} \in Edg (G))$
32	30 31	syl5bir	$⊢ G \in ComplUSGraph \to (((b \in V \land c \in V) \land b \neq c) \to \{b, c\} \in Edg (G))$
33	29 32	anim12d	$⊢ G \in ComplUSGraph \to ((((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c)) \land ((b \in V \land c \in V) \land b \neq c)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)) \land \{b, c\} \in Edg (G)))$
34	16 33	syl5	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)) \land \{b, c\} \in Edg (G)))$
35		3anan32	$⊢ (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{a, c\} \in Edg (G)) \leftrightarrow ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)) \land \{b, c\} \in Edg (G))$
36		prcom	$⊢ \{a, c\} = \{c, a\}$
37	36	eleq1i	$⊢ \{a, c\} \in Edg (G) \leftrightarrow \{c, a\} \in Edg (G)$
38	37	3anbi3i	$⊢ (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{a, c\} \in Edg (G)) \leftrightarrow (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))$
39	35 38	bitr3i	$⊢ ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G)) \land \{b, c\} \in Edg (G)) \leftrightarrow (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))$
40	34 39	syl6ib	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G)))$
41		pm5.3	$⊢ (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))) \leftrightarrow (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to ((a \in V \land b \in V \land c \in V) \land (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))))$
42	40 41	sylib	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to ((a \in V \land b \in V \land c \in V) \land (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))))$
43	1 22	umgr3cyclex	$⊢ (G \in UMGraph \land (a \in V \land b \in V \land c \in V) \land (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = a)$
44		3simpa	$⊢ (f Cycles (G) p \land \|f\| = 3 \land p (0) = a) \to (f Cycles (G) p \land \|f\| = 3)$
45	44	2eximi	$⊢ \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = a) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
46	43 45	syl	$⊢ (G \in UMGraph \land (a \in V \land b \in V \land c \in V) \land (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
47	46	3expib	$⊢ G \in UMGraph \to (((a \in V \land b \in V \land c \in V) \land (\{a, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, a\} \in Edg (G))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
48	6 42 47	sylsyld	$⊢ G \in ComplUSGraph \to (((a \in V \land b \in V \land c \in V) \land (a \neq b \land a \neq c \land b \neq c)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
49	48	expdimp	$⊢ (G \in ComplUSGraph \land (a \in V \land b \in V \land c \in V)) \to ((a \neq b \land a \neq c \land b \neq c) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
50	3 49	sylbir	$⊢ ((G \in ComplUSGraph \land a \in V) \land (b \in V \land c \in V)) \to ((a \neq b \land a \neq c \land b \neq c) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
51	50	reximdvva	$⊢ (G \in ComplUSGraph \land a \in V) \to (\exists b \in V \exists c \in V (a \neq b \land a \neq c \land b \neq c) \to \exists b \in V \exists c \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
52	51	reximdva	$⊢ G \in ComplUSGraph \to (\exists a \in V \exists b \in V \exists c \in V (a \neq b \land a \neq c \land b \neq c) \to \exists a \in V \exists b \in V \exists c \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
53		id	$⊢ \exists f \exists p (f Cycles (G) p \land \|f\| = 3) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
54	53	rexlimivw	$⊢ \exists c \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
55	54	rexlimivw	$⊢ \exists b \in V \exists c \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
56	55	rexlimivw	$⊢ \exists a \in V \exists b \in V \exists c \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$
57	52 56	syl6	$⊢ G \in ComplUSGraph \to (\exists a \in V \exists b \in V \exists c \in V (a \neq b \land a \neq c \land b \neq c) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3))$
58	1	fvexi	$⊢ V \in V$
59		hashgt23el	$⊢ (V \in V \land 2 < \|V\|) \to \exists a \in V \exists b \in V \exists c \in V (a \neq b \land a \neq c \land b \neq c)$
60	58 59	mpan	$⊢ 2 < \|V\| \to \exists a \in V \exists b \in V \exists c \in V (a \neq b \land a \neq c \land b \neq c)$
61	57 60	impel	$⊢ (G \in ComplUSGraph \land 2 < \|V\|) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3)$

Metamath Proof Explorer

Theorem cusgr3cyclex

Proof