upgr3v3e3cycl

Description: If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017)

	Ref	Expression
Hypotheses	upgr3v3e3cycl.e	$⊢ E = Edg (G)$
	upgr3v3e3cycl.v	$⊢ V = Vtx (G)$
Assertion	upgr3v3e3cycl	$⊢ (G \in UPGraph \land F Cycles (G) P \land \|F\| = 3) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))$

Proof

Step	Hyp	Ref	Expression
1		upgr3v3e3cycl.e	$⊢ E = Edg (G)$
2		upgr3v3e3cycl.v	$⊢ V = Vtx (G)$
3		cyclprop	$⊢ F Cycles (G) P \to (F Paths (G) P \land P (0) = P (\|F\|))$
4		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
5	1	upgrwlkvtxedg	$⊢ (G \in UPGraph \land F Walks (G) P) \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E$
6		fveq2	$⊢ \|F\| = 3 \to P (\|F\|) = P (3)$
7	6	eqeq2d	$⊢ \|F\| = 3 \to (P (0) = P (\|F\|) \leftrightarrow P (0) = P (3))$
8	7	anbi2d	$⊢ \|F\| = 3 \to ((F Paths (G) P \land P (0) = P (\|F\|)) \leftrightarrow (F Paths (G) P \land P (0) = P (3)))$
9		oveq2	$⊢ \|F\| = 3 \to (0 ..^\|F\|) = (0 ..^3)$
10		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
11	9 10	eqtrdi	$⊢ \|F\| = 3 \to (0 ..^\|F\|) = \{0, 1, 2\}$
12	11	raleqdv	$⊢ \|F\| = 3 \to (\forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E \leftrightarrow \forall k \in \{0, 1, 2\} \{P (k), P (k + 1)\} \in E)$
13		c0ex	$⊢ 0 \in V$
14		1ex	$⊢ 1 \in V$
15		2ex	$⊢ 2 \in V$
16		fveq2	$⊢ k = 0 \to P (k) = P (0)$
17		fv0p1e1	$⊢ k = 0 \to P (k + 1) = P (1)$
18	16 17	preq12d	$⊢ k = 0 \to \{P (k), P (k + 1)\} = \{P (0), P (1)\}$
19	18	eleq1d	$⊢ k = 0 \to (\{P (k), P (k + 1)\} \in E \leftrightarrow \{P (0), P (1)\} \in E)$
20		fveq2	$⊢ k = 1 \to P (k) = P (1)$
21		oveq1	$⊢ k = 1 \to k + 1 = 1 + 1$
22		1p1e2	$⊢ 1 + 1 = 2$
23	21 22	eqtrdi	$⊢ k = 1 \to k + 1 = 2$
24	23	fveq2d	$⊢ k = 1 \to P (k + 1) = P (2)$
25	20 24	preq12d	$⊢ k = 1 \to \{P (k), P (k + 1)\} = \{P (1), P (2)\}$
26	25	eleq1d	$⊢ k = 1 \to (\{P (k), P (k + 1)\} \in E \leftrightarrow \{P (1), P (2)\} \in E)$
27		fveq2	$⊢ k = 2 \to P (k) = P (2)$
28		oveq1	$⊢ k = 2 \to k + 1 = 2 + 1$
29		2p1e3	$⊢ 2 + 1 = 3$
30	28 29	eqtrdi	$⊢ k = 2 \to k + 1 = 3$
31	30	fveq2d	$⊢ k = 2 \to P (k + 1) = P (3)$
32	27 31	preq12d	$⊢ k = 2 \to \{P (k), P (k + 1)\} = \{P (2), P (3)\}$
33	32	eleq1d	$⊢ k = 2 \to (\{P (k), P (k + 1)\} \in E \leftrightarrow \{P (2), P (3)\} \in E)$
34	13 14 15 19 26 33	raltp	$⊢ \forall k \in \{0, 1, 2\} \{P (k), P (k + 1)\} \in E \leftrightarrow (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)$
35	12 34	bitrdi	$⊢ \|F\| = 3 \to (\forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E \leftrightarrow (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E))$
36	8 35	anbi12d	$⊢ \|F\| = 3 \to (((F Paths (G) P \land P (0) = P (\|F\|)) \land \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E) \leftrightarrow ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)))$
37	2	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
38		oveq2	$⊢ \|F\| = 3 \to (0 \dots \|F\|) = (0 \dots 3)$
39	38	feq2d	$⊢ \|F\| = 3 \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 3) ⟶ V)$
40		id	$⊢ P : (0 \dots 3) ⟶ V \to P : (0 \dots 3) ⟶ V$
41		3nn0	$⊢ 3 \in ℕ_{0}$
42		0elfz	$⊢ 3 \in ℕ_{0} \to 0 \in (0 \dots 3)$
43	41 42	mp1i	$⊢ P : (0 \dots 3) ⟶ V \to 0 \in (0 \dots 3)$
44	40 43	ffvelrnd	$⊢ P : (0 \dots 3) ⟶ V \to P (0) \in V$
45		1nn0	$⊢ 1 \in ℕ_{0}$
46		1lt3	$⊢ 1 < 3$
47		fvffz0	$⊢ ((3 \in ℕ_{0} \land 1 \in ℕ_{0} \land 1 < 3) \land P : (0 \dots 3) ⟶ V) \to P (1) \in V$
48	47	ex	$⊢ (3 \in ℕ_{0} \land 1 \in ℕ_{0} \land 1 < 3) \to (P : (0 \dots 3) ⟶ V \to P (1) \in V)$
49	41 45 46 48	mp3an	$⊢ P : (0 \dots 3) ⟶ V \to P (1) \in V$
50		2nn0	$⊢ 2 \in ℕ_{0}$
51		2lt3	$⊢ 2 < 3$
52		fvffz0	$⊢ ((3 \in ℕ_{0} \land 2 \in ℕ_{0} \land 2 < 3) \land P : (0 \dots 3) ⟶ V) \to P (2) \in V$
53	52	ex	$⊢ (3 \in ℕ_{0} \land 2 \in ℕ_{0} \land 2 < 3) \to (P : (0 \dots 3) ⟶ V \to P (2) \in V)$
54	41 50 51 53	mp3an	$⊢ P : (0 \dots 3) ⟶ V \to P (2) \in V$
55	44 49 54	3jca	$⊢ P : (0 \dots 3) ⟶ V \to (P (0) \in V \land P (1) \in V \land P (2) \in V)$
56	39 55	syl6bi	$⊢ \|F\| = 3 \to (P : (0 \dots \|F\|) ⟶ V \to (P (0) \in V \land P (1) \in V \land P (2) \in V))$
57	56	com12	$⊢ P : (0 \dots \|F\|) ⟶ V \to (\|F\| = 3 \to (P (0) \in V \land P (1) \in V \land P (2) \in V))$
58	4 37 57	3syl	$⊢ F Paths (G) P \to (\|F\| = 3 \to (P (0) \in V \land P (1) \in V \land P (2) \in V))$
59	58	adantr	$⊢ (F Paths (G) P \land P (0) = P (3)) \to (\|F\| = 3 \to (P (0) \in V \land P (1) \in V \land P (2) \in V))$
60	59	adantr	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)) \to (\|F\| = 3 \to (P (0) \in V \land P (1) \in V \land P (2) \in V))$
61	60	impcom	$⊢ (\|F\| = 3 \land ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E))) \to (P (0) \in V \land P (1) \in V \land P (2) \in V)$
62		preq2	$⊢ P (3) = P (0) \to \{P (2), P (3)\} = \{P (2), P (0)\}$
63	62	eqcoms	$⊢ P (0) = P (3) \to \{P (2), P (3)\} = \{P (2), P (0)\}$
64	63	adantl	$⊢ (F Paths (G) P \land P (0) = P (3)) \to \{P (2), P (3)\} = \{P (2), P (0)\}$
65	64	eleq1d	$⊢ (F Paths (G) P \land P (0) = P (3)) \to (\{P (2), P (3)\} \in E \leftrightarrow \{P (2), P (0)\} \in E)$
66	65	3anbi3d	$⊢ (F Paths (G) P \land P (0) = P (3)) \to ((\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E) \leftrightarrow (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E))$
67	66	biimpa	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)) \to (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E)$
68	67	adantl	$⊢ (\|F\| = 3 \land ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E))) \to (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E)$
69		simpll	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to F Paths (G) P$
70		breq2	$⊢ \|F\| = 3 \to (1 < \|F\| \leftrightarrow 1 < 3)$
71	46 70	mpbiri	$⊢ \|F\| = 3 \to 1 < \|F\|$
72	71	adantl	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to 1 < \|F\|$
73		3nn	$⊢ 3 \in ℕ$
74		lbfzo0	$⊢ 0 \in (0 ..^3) \leftrightarrow 3 \in ℕ$
75	73 74	mpbir	$⊢ 0 \in (0 ..^3)$
76	75 9	eleqtrrid	$⊢ \|F\| = 3 \to 0 \in (0 ..^\|F\|)$
77	76	adantl	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to 0 \in (0 ..^\|F\|)$
78		pthdadjvtx	$⊢ (F Paths (G) P \land 1 < \|F\| \land 0 \in (0 ..^\|F\|)) \to P (0) \neq P (0 + 1)$
79		1e0p1	$⊢ 1 = 0 + 1$
80	79	fveq2i	$⊢ P (1) = P (0 + 1)$
81	80	neeq2i	$⊢ P (0) \neq P (1) \leftrightarrow P (0) \neq P (0 + 1)$
82	78 81	sylibr	$⊢ (F Paths (G) P \land 1 < \|F\| \land 0 \in (0 ..^\|F\|)) \to P (0) \neq P (1)$
83	69 72 77 82	syl3anc	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to P (0) \neq P (1)$
84		elfzo0	$⊢ 1 \in (0 ..^3) \leftrightarrow (1 \in ℕ_{0} \land 3 \in ℕ \land 1 < 3)$
85	45 73 46 84	mpbir3an	$⊢ 1 \in (0 ..^3)$
86	85 9	eleqtrrid	$⊢ \|F\| = 3 \to 1 \in (0 ..^\|F\|)$
87	86	adantl	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to 1 \in (0 ..^\|F\|)$
88		pthdadjvtx	$⊢ (F Paths (G) P \land 1 < \|F\| \land 1 \in (0 ..^\|F\|)) \to P (1) \neq P (1 + 1)$
89		df-2	$⊢ 2 = 1 + 1$
90	89	fveq2i	$⊢ P (2) = P (1 + 1)$
91	90	neeq2i	$⊢ P (1) \neq P (2) \leftrightarrow P (1) \neq P (1 + 1)$
92	88 91	sylibr	$⊢ (F Paths (G) P \land 1 < \|F\| \land 1 \in (0 ..^\|F\|)) \to P (1) \neq P (2)$
93	69 72 87 92	syl3anc	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to P (1) \neq P (2)$
94		elfzo0	$⊢ 2 \in (0 ..^3) \leftrightarrow (2 \in ℕ_{0} \land 3 \in ℕ \land 2 < 3)$
95	50 73 51 94	mpbir3an	$⊢ 2 \in (0 ..^3)$
96	95 9	eleqtrrid	$⊢ \|F\| = 3 \to 2 \in (0 ..^\|F\|)$
97	96	adantl	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to 2 \in (0 ..^\|F\|)$
98		pthdadjvtx	$⊢ (F Paths (G) P \land 1 < \|F\| \land 2 \in (0 ..^\|F\|)) \to P (2) \neq P (2 + 1)$
99	69 72 97 98	syl3anc	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to P (2) \neq P (2 + 1)$
100		neeq2	$⊢ P (0) = P (3) \to (P (2) \neq P (0) \leftrightarrow P (2) \neq P (3))$
101		df-3	$⊢ 3 = 2 + 1$
102	101	fveq2i	$⊢ P (3) = P (2 + 1)$
103	102	neeq2i	$⊢ P (2) \neq P (3) \leftrightarrow P (2) \neq P (2 + 1)$
104	100 103	bitrdi	$⊢ P (0) = P (3) \to (P (2) \neq P (0) \leftrightarrow P (2) \neq P (2 + 1))$
105	104	adantl	$⊢ (F Paths (G) P \land P (0) = P (3)) \to (P (2) \neq P (0) \leftrightarrow P (2) \neq P (2 + 1))$
106	105	adantr	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to (P (2) \neq P (0) \leftrightarrow P (2) \neq P (2 + 1))$
107	99 106	mpbird	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to P (2) \neq P (0)$
108	83 93 107	3jca	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land \|F\| = 3) \to (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0))$
109	108	ex	$⊢ (F Paths (G) P \land P (0) = P (3)) \to (\|F\| = 3 \to (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0)))$
110	109	adantr	$⊢ ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)) \to (\|F\| = 3 \to (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0)))$
111	110	impcom	$⊢ (\|F\| = 3 \land ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E))) \to (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0))$
112		preq1	$⊢ a = P (0) \to \{a, b\} = \{P (0), b\}$
113	112	eleq1d	$⊢ a = P (0) \to (\{a, b\} \in E \leftrightarrow \{P (0), b\} \in E)$
114		preq2	$⊢ a = P (0) \to \{c, a\} = \{c, P (0)\}$
115	114	eleq1d	$⊢ a = P (0) \to (\{c, a\} \in E \leftrightarrow \{c, P (0)\} \in E)$
116	113 115	3anbi13d	$⊢ a = P (0) \to ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \leftrightarrow (\{P (0), b\} \in E \land \{b, c\} \in E \land \{c, P (0)\} \in E))$
117		neeq1	$⊢ a = P (0) \to (a \neq b \leftrightarrow P (0) \neq b)$
118		neeq2	$⊢ a = P (0) \to (c \neq a \leftrightarrow c \neq P (0))$
119	117 118	3anbi13d	$⊢ a = P (0) \to ((a \neq b \land b \neq c \land c \neq a) \leftrightarrow (P (0) \neq b \land b \neq c \land c \neq P (0)))$
120	116 119	anbi12d	$⊢ a = P (0) \to (((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)) \leftrightarrow ((\{P (0), b\} \in E \land \{b, c\} \in E \land \{c, P (0)\} \in E) \land (P (0) \neq b \land b \neq c \land c \neq P (0))))$
121		preq2	$⊢ b = P (1) \to \{P (0), b\} = \{P (0), P (1)\}$
122	121	eleq1d	$⊢ b = P (1) \to (\{P (0), b\} \in E \leftrightarrow \{P (0), P (1)\} \in E)$
123		preq1	$⊢ b = P (1) \to \{b, c\} = \{P (1), c\}$
124	123	eleq1d	$⊢ b = P (1) \to (\{b, c\} \in E \leftrightarrow \{P (1), c\} \in E)$
125	122 124	3anbi12d	$⊢ b = P (1) \to ((\{P (0), b\} \in E \land \{b, c\} \in E \land \{c, P (0)\} \in E) \leftrightarrow (\{P (0), P (1)\} \in E \land \{P (1), c\} \in E \land \{c, P (0)\} \in E))$
126		neeq2	$⊢ b = P (1) \to (P (0) \neq b \leftrightarrow P (0) \neq P (1))$
127		neeq1	$⊢ b = P (1) \to (b \neq c \leftrightarrow P (1) \neq c)$
128	126 127	3anbi12d	$⊢ b = P (1) \to ((P (0) \neq b \land b \neq c \land c \neq P (0)) \leftrightarrow (P (0) \neq P (1) \land P (1) \neq c \land c \neq P (0)))$
129	125 128	anbi12d	$⊢ b = P (1) \to (((\{P (0), b\} \in E \land \{b, c\} \in E \land \{c, P (0)\} \in E) \land (P (0) \neq b \land b \neq c \land c \neq P (0))) \leftrightarrow ((\{P (0), P (1)\} \in E \land \{P (1), c\} \in E \land \{c, P (0)\} \in E) \land (P (0) \neq P (1) \land P (1) \neq c \land c \neq P (0))))$
130		preq2	$⊢ c = P (2) \to \{P (1), c\} = \{P (1), P (2)\}$
131	130	eleq1d	$⊢ c = P (2) \to (\{P (1), c\} \in E \leftrightarrow \{P (1), P (2)\} \in E)$
132		preq1	$⊢ c = P (2) \to \{c, P (0)\} = \{P (2), P (0)\}$
133	132	eleq1d	$⊢ c = P (2) \to (\{c, P (0)\} \in E \leftrightarrow \{P (2), P (0)\} \in E)$
134	131 133	3anbi23d	$⊢ c = P (2) \to ((\{P (0), P (1)\} \in E \land \{P (1), c\} \in E \land \{c, P (0)\} \in E) \leftrightarrow (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E))$
135		neeq2	$⊢ c = P (2) \to (P (1) \neq c \leftrightarrow P (1) \neq P (2))$
136		neeq1	$⊢ c = P (2) \to (c \neq P (0) \leftrightarrow P (2) \neq P (0))$
137	135 136	3anbi23d	$⊢ c = P (2) \to ((P (0) \neq P (1) \land P (1) \neq c \land c \neq P (0)) \leftrightarrow (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0)))$
138	134 137	anbi12d	$⊢ c = P (2) \to (((\{P (0), P (1)\} \in E \land \{P (1), c\} \in E \land \{c, P (0)\} \in E) \land (P (0) \neq P (1) \land P (1) \neq c \land c \neq P (0))) \leftrightarrow ((\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E) \land (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0))))$
139	120 129 138	rspc3ev	$⊢ ((P (0) \in V \land P (1) \in V \land P (2) \in V) \land ((\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (0)\} \in E) \land (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (0)))) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))$
140	61 68 111 139	syl12anc	$⊢ (\|F\| = 3 \land ((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E))) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))$
141	140	ex	$⊢ \|F\| = 3 \to (((F Paths (G) P \land P (0) = P (3)) \land (\{P (0), P (1)\} \in E \land \{P (1), P (2)\} \in E \land \{P (2), P (3)\} \in E)) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)))$
142	36 141	sylbid	$⊢ \|F\| = 3 \to (((F Paths (G) P \land P (0) = P (\|F\|)) \land \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)))$
143	142	expd	$⊢ \|F\| = 3 \to ((F Paths (G) P \land P (0) = P (\|F\|)) \to (\forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))$
144	143	com13	$⊢ \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \in E \to ((F Paths (G) P \land P (0) = P (\|F\|)) \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))$
145	5 144	syl	$⊢ (G \in UPGraph \land F Walks (G) P) \to ((F Paths (G) P \land P (0) = P (\|F\|)) \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))$
146	145	expcom	$⊢ F Walks (G) P \to (G \in UPGraph \to ((F Paths (G) P \land P (0) = P (\|F\|)) \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)))))$
147	146	com23	$⊢ F Walks (G) P \to ((F Paths (G) P \land P (0) = P (\|F\|)) \to (G \in UPGraph \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)))))$
148	147	expd	$⊢ F Walks (G) P \to (F Paths (G) P \to (P (0) = P (\|F\|) \to (G \in UPGraph \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))))$
149	4 148	mpcom	$⊢ F Paths (G) P \to (P (0) = P (\|F\|) \to (G \in UPGraph \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a)))))$
150	149	imp	$⊢ (F Paths (G) P \land P (0) = P (\|F\|)) \to (G \in UPGraph \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))$
151	3 150	syl	$⊢ F Cycles (G) P \to (G \in UPGraph \to (\|F\| = 3 \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))))$
152	151	3imp21	$⊢ (G \in UPGraph \land F Cycles (G) P \land \|F\| = 3) \to \exists a \in V \exists b \in V \exists c \in V ((\{a, b\} \in E \land \{b, c\} \in E \land \{c, a\} \in E) \land (a \neq b \land b \neq c \land c \neq a))$

Metamath Proof Explorer

Theorem upgr3v3e3cycl

Proof