upgr3v3e3cycl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > upgr3v3e3cycl		Structured version Visualization version GIF version

Theorem upgr3v3e3cycl 27360

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.)

**Hypotheses**
Ref	Expression
upgr3v3e3cycl.e	⊢ 𝐸 = (Edg‘𝐺)
upgr3v3e3cycl.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
upgr3v3e3cycl	⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))

Distinct variable groups: 𝐸,𝑎,𝑏,𝑐 𝑃,𝑎,𝑏,𝑐 𝑉,𝑎,𝑏,𝑐 Allowed substitution hints: 𝐹(𝑎,𝑏,𝑐) 𝐺(𝑎,𝑏,𝑐)

Proof of Theorem upgr3v3e3cycl Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cyclprop 26924	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 26858	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr3v3e3cycl.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 26776	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6332	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3))
6	5	eqeq2d 2781	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
7	6	anbi2d 614	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8		oveq2 6801	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = (0..^3))
9		fzo0to3tp 12762	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) = {0, 1, 2}
10	8, 9	syl6eq 2821	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = {0, 1, 2})
11	10	raleqdv 3293	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		c0ex 10236	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
13		1ex 10237	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
14		2ex 11294	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ V
15		fveq2 6332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		oveq1 6800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17		0p1e1 11334	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 + 1) = 1
18	16, 17	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → (𝑘 + 1) = 1)
19	18	fveq2d 6336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
20	15, 19	preq12d 4412	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
21	20	eleq1d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22		fveq2 6332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
23		oveq1 6800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24		1p1e2 11336	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
25	23, 24	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
26	25	fveq2d 6336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
27	22, 26	preq12d 4412	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
28	27	eleq1d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
29		fveq2 6332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 6800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 11353	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 + 1) = 3
32	30, 31	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4412	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36	12, 13, 14, 21, 28, 35	raltp 4377	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
37	11, 36	syl6bb 276	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))
38	7, 37	anbi12d 616	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
39		upgr3v3e3cycl.v	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 = (Vtx‘𝐺)
40	39	wlkp 26747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
41		oveq2 6801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (0...(♯‘𝐹)) = (0...3))
42	41	feq2d 6171	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉))
43		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉)
44		3nn0 11512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℕ₀
45		0elfz 12644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 ∈ ℕ₀ → 0 ∈ (0...3))
46	44, 45	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
47	43, 46	ffvelrnd 6503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
48		1nn0 11510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ₀
49		1lt3 11398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < 3
50		fvffz0 12665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
51	50	ex 397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
52	44, 48, 49, 51	mp3an 1572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
53		2nn0 11511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ₀
54		2lt3 11397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 < 3
55		fvffz0 12665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
56	55	ex 397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
57	44, 53, 54, 56	mp3an 1572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
58	47, 52, 57	3jca 1122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
59	42, 58	syl6bi 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
60	59	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
61	2, 40, 60	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
62	61	adantr 466	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
63	62	adantr 466	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
64	63	impcom 394	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
65		preq2 4405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
66	65	eqcoms 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
67	66	adantl 467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
68	67	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69	68	3anbi3d 1553	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
70	69	biimpa 462	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
71	70	adantl 467	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
72		simpll 750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃)
73		breq2 4790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (1 < (♯‘𝐹) ↔ 1 < 3))
74	49, 73	mpbiri 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 < (♯‘𝐹))
75	74	adantl 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 < (♯‘𝐹))
76		3nn 11388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℕ
77		lbfzo0 12716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
78	76, 77	mpbir 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ (0..^3)
79	78, 8	syl5eleqr 2857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 0 ∈ (0..^(♯‘𝐹)))
80	79	adantl 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈ (0..^(♯‘𝐹)))
81		pthdadjvtx 26861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82		1e0p1 11754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 = (0 + 1)
83	82	fveq2i 6335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
84	83	neeq2i 3008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
85	81, 84	sylibr 224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
86	72, 75, 80, 85	syl3anc 1476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
87		elfzo0 12717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ (0..^3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 1 < 3))
88	48, 76, 49, 87	mpbir3an 1426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ (0..^3)
89	88, 8	syl5eleqr 2857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 ∈ (0..^(♯‘𝐹)))
90	89	adantl 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈ (0..^(♯‘𝐹)))
91		pthdadjvtx 26861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92		df-2 11281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 = (1 + 1)
93	92	fveq2i 6335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
94	93	neeq2i 3008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
95	91, 94	sylibr 224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
96	72, 75, 90, 95	syl3anc 1476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
97		elfzo0 12717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ (0..^3) ↔ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 2 < 3))
98	53, 76, 54, 97	mpbir3an 1426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (0..^3)
99	98, 8	syl5eleqr 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → 2 ∈ (0..^(♯‘𝐹)))
100	99	adantl 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈ (0..^(♯‘𝐹)))
101		pthdadjvtx 26861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
102	72, 75, 100, 101	syl3anc 1476	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
103		neeq2 3006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
104		df-3 11282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
105	104	fveq2i 6335	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
106	105	neeq2i 3008	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
107	103, 106	syl6bb 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
108	107	adantl 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
109	108	adantr 466	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
110	102, 109	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
111	86, 96, 110	3jca 1122	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112	111	ex 397	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
113	112	adantr 466	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
114	113	impcom 394	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
115		preq1 4404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
116	115	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
117		preq2 4405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
118	117	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
119	116, 118	3anbi13d 1549	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
120		neeq1 3005	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
121		neeq2 3006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0)))
122	120, 121	3anbi13d 1549	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
123	119, 122	anbi12d 616	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
124		preq2 4405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
125	124	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
126		preq1 4404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
127	126	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
128	125, 127	3anbi12d 1548	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
129		neeq2 3006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
130		neeq1 3005	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
131	129, 130	3anbi12d 1548	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
132	128, 131	anbi12d 616	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
133		preq2 4405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
134	133	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
135		preq1 4404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
136	135	eleq1d 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
137	134, 136	3anbi23d 1550	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
138		neeq2 3006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
139		neeq1 3005	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
140	138, 139	3anbi23d 1550	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
141	137, 140	anbi12d 616	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))))
142	123, 132, 141	rspc3ev 3476	. . . . . . . . . . . . . 14 ⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
143	64, 71, 114, 142	syl12anc 1474	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
144	143	ex 397	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
145	38, 144	sylbid 230	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
146	145	expd 400	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
147	146	com13 88	. . . . . . . . 9 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
148	4, 147	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
149	148	expcom 398	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
150	149	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
151	150	expd 400	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))))
152	2, 151	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
153	152	imp 393	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
154	1, 153	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
155	154	3imp21 1105	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∃wrex 3062 {cpr 4318 {ctp 4320 class class class wbr 4786 ⟶wf 6027 ‘cfv 6031 (class class class)co 6793 0cc0 10138 1c1 10139 + caddc 10141 < clt 10276 ℕcn 11222 2c2 11272 3c3 11273 ℕ₀cn0 11494 ...cfz 12533 ..^cfzo 12673 ♯chash 13321 Vtxcvtx 26095 Edgcedg 26160 UPGraphcupgr 26196 Walkscwlks 26727 Pathscpths 26843 Cyclesccycls 26916

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-cnex 10194 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 ax-pre-mulgt0 10215

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-ifp 1050 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6754 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-1o 7713 df-2o 7714 df-oadd 7717 df-er 7896 df-map 8011 df-pm 8012 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-card 8965 df-cda 9192 df-pnf 10278 df-mnf 10279 df-xr 10280 df-ltxr 10281 df-le 10282 df-sub 10470 df-neg 10471 df-nn 11223 df-2 11281 df-3 11282 df-n0 11495 df-xnn0 11566 df-z 11580 df-uz 11889 df-fz 12534 df-fzo 12674 df-hash 13322 df-word 13495 df-edg 26161 df-uhgr 26174 df-upgr 26198 df-wlks 26730 df-trls 26824 df-pths 26847 df-cycls 26918

This theorem is referenced by: umgr3v3e3cycl 27364

W3C validator