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 28235

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 27852	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 27786	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr3v3e3cycl.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 27704	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6706	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3))
6	5	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
7	6	anbi2d 632	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8		oveq2 7210	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = (0..^3))
9		fzo0to3tp 13311	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) = {0, 1, 2}
10	8, 9	eqtrdi 2790	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = {0, 1, 2})
11	10	raleqdv 3318	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		c0ex 10810	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
13		1ex 10812	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
14		2ex 11890	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ V
15		fveq2 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 11936	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4647	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7209	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 11938	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6710	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4647	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26		fveq2 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
27		oveq1 7209	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
28		2p1e3 11955	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 + 1) = 3
29	27, 28	eqtrdi 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
30	29	fveq2d 6710	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
31	26, 30	preq12d 4647	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
32	31	eleq1d 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
33	12, 13, 14, 18, 25, 32	raltp 4611	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
34	11, 33	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))
35	7, 34	anbi12d 634	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
36		upgr3v3e3cycl.v	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 = (Vtx‘𝐺)
37	36	wlkp 27676	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
38		oveq2 7210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (0...(♯‘𝐹)) = (0...3))
39	38	feq2d 6520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉))
40		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉)
41		3nn0 12091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℕ₀
42		0elfz 13192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 ∈ ℕ₀ → 0 ∈ (0...3))
43	41, 42	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
44	40, 43	ffvelrnd 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
45		1nn0 12089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ₀
46		1lt3 11986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < 3
47		fvffz0 13213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
48	47	ex 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
49	41, 45, 46, 48	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
50		2nn0 12090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ₀
51		2lt3 11985	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 < 3
52		fvffz0 13213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
53	52	ex 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
54	41, 50, 51, 53	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
55	44, 49, 54	3jca 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
56	39, 55	syl6bi 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
57	56	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
58	2, 37, 57	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
59	58	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
60	59	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
61	60	impcom 411	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
62		preq2 4640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
63	62	eqcoms 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
64	63	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
65	64	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
66	65	3anbi3d 1444	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
67	66	biimpa 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
68	67	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69		simpll 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃)
70		breq2 5047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (1 < (♯‘𝐹) ↔ 1 < 3))
71	46, 70	mpbiri 261	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 < (♯‘𝐹))
72	71	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 < (♯‘𝐹))
73		3nn 11892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℕ
74		lbfzo0 13265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
75	73, 74	mpbir 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ (0..^3)
76	75, 8	eleqtrrid 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 0 ∈ (0..^(♯‘𝐹)))
77	76	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈ (0..^(♯‘𝐹)))
78		pthdadjvtx 27789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
79		1e0p1 12318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 = (0 + 1)
80	79	fveq2i 6709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
81	80	neeq2i 3000	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82	78, 81	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
83	69, 72, 77, 82	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
84		elfzo0 13266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ (0..^3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 1 < 3))
85	45, 73, 46, 84	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ (0..^3)
86	85, 8	eleqtrrid 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 ∈ (0..^(♯‘𝐹)))
87	86	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈ (0..^(♯‘𝐹)))
88		pthdadjvtx 27789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
89		df-2 11876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 = (1 + 1)
90	89	fveq2i 6709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
91	90	neeq2i 3000	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92	88, 91	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
93	69, 72, 87, 92	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
94		elfzo0 13266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ (0..^3) ↔ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 2 < 3))
95	50, 73, 51, 94	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (0..^3)
96	95, 8	eleqtrrid 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → 2 ∈ (0..^(♯‘𝐹)))
97	96	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈ (0..^(♯‘𝐹)))
98		pthdadjvtx 27789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
99	69, 72, 97, 98	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
100		neeq2 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
101		df-3 11877	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
102	101	fveq2i 6709	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
103	102	neeq2i 3000	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
104	100, 103	bitrdi 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
105	104	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
106	105	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
107	99, 106	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
108	83, 93, 107	3jca 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
109	108	ex 416	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
110	109	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
111	110	impcom 411	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112		preq1 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
113	112	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
114		preq2 4640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
115	114	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
116	113, 115	3anbi13d 1440	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
117		neeq1 2997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
118		neeq2 2998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0)))
119	117, 118	3anbi13d 1440	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
120	116, 119	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
121		preq2 4640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
122	121	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
123		preq1 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
124	123	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
125	122, 124	3anbi12d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
126		neeq2 2998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
127		neeq1 2997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
128	126, 127	3anbi12d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
129	125, 128	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
130		preq2 4640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
131	130	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
132		preq1 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
133	132	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
134	131, 133	3anbi23d 1441	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
135		neeq2 2998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
136		neeq1 2997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
137	135, 136	3anbi23d 1441	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
138	134, 137	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))))
139	120, 129, 138	rspc3ev 3544	. . . . . . . . . . . . . 14 ⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
140	61, 68, 111, 139	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
141	140	ex 416	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
142	35, 141	sylbid 243	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
143	142	expd 419	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
144	143	com13 88	. . . . . . . . 9 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
145	4, 144	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
146	145	expcom 417	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
147	146	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
148	147	expd 419	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))))
149	2, 148	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
150	149	imp 410	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
151	1, 150	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
152	151	3imp21 1116	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ∀wral 3054 ∃wrex 3055 {cpr 4533 {ctp 4535 class class class wbr 5043 ⟶wf 6365 ‘cfv 6369 (class class class)co 7202 0cc0 10712 1c1 10713 + caddc 10715 < clt 10850 ℕcn 11813 2c2 11868 3c3 11869 ℕ₀cn0 12073 ...cfz 13078 ..^cfzo 13221 ♯chash 13879 Vtxcvtx 27059 Edgcedg 27110 UPGraphcupgr 27143 Walkscwlks 27656 Pathscpths 27771 Cyclesccycls 27844

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-ifp 1064 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-om 7634 df-1st 7750 df-2nd 7751 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-oadd 8195 df-er 8380 df-map 8499 df-pm 8500 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-dju 9500 df-card 9538 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-nn 11814 df-2 11876 df-3 11877 df-n0 12074 df-xnn0 12146 df-z 12160 df-uz 12422 df-fz 13079 df-fzo 13222 df-hash 13880 df-word 14053 df-edg 27111 df-uhgr 27121 df-upgr 27145 df-wlks 27659 df-trls 27752 df-pths 27775 df-cycls 27846

This theorem is referenced by: umgr3v3e3cycl 28239

W3C validator