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 28540

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 28157	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 28091	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr3v3e3cycl.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 28009	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6771	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3))
6	5	eqeq2d 2751	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
7	6	anbi2d 629	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8		oveq2 7279	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = (0..^3))
9		fzo0to3tp 13471	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) = {0, 1, 2}
10	8, 9	eqtrdi 2796	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = {0, 1, 2})
11	10	raleqdv 3347	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		c0ex 10970	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
13		1ex 10972	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
14		2ex 12050	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ V
15		fveq2 6771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 12096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4683	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 12098	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4683	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26		fveq2 6771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
27		oveq1 7278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
28		2p1e3 12115	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 + 1) = 3
29	27, 28	eqtrdi 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
30	29	fveq2d 6775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
31	26, 30	preq12d 4683	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
32	31	eleq1d 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
33	12, 13, 14, 18, 25, 32	raltp 4647	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
34	11, 33	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))
35	7, 34	anbi12d 631	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
36		upgr3v3e3cycl.v	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 = (Vtx‘𝐺)
37	36	wlkp 27981	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
38		oveq2 7279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (0...(♯‘𝐹)) = (0...3))
39	38	feq2d 6584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉))
40		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉)
41		3nn0 12251	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℕ₀
42		0elfz 13352	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 ∈ ℕ₀ → 0 ∈ (0...3))
43	41, 42	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
44	40, 43	ffvelrnd 6959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
45		1nn0 12249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ₀
46		1lt3 12146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < 3
47		fvffz0 13373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
48	47	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
49	41, 45, 46, 48	mp3an 1460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
50		2nn0 12250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ₀
51		2lt3 12145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 < 3
52		fvffz0 13373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
53	52	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
54	41, 50, 51, 53	mp3an 1460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
55	44, 49, 54	3jca 1127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
56	39, 55	syl6bi 252	. . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
60	59	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
61	60	impcom 408	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
62		preq2 4676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
63	62	eqcoms 2748	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
64	63	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
65	64	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
66	65	3anbi3d 1441	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
67	66	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
68	67	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69		simpll 764	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃)
70		breq2 5083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (1 < (♯‘𝐹) ↔ 1 < 3))
71	46, 70	mpbiri 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 < (♯‘𝐹))
72	71	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 < (♯‘𝐹))
73		3nn 12052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℕ
74		lbfzo0 13425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
75	73, 74	mpbir 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ (0..^3)
76	75, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 0 ∈ (0..^(♯‘𝐹)))
77	76	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈ (0..^(♯‘𝐹)))
78		pthdadjvtx 28094	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
79		1e0p1 12478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 = (0 + 1)
80	79	fveq2i 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
81	80	neeq2i 3011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82	78, 81	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
83	69, 72, 77, 82	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
84		elfzo0 13426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ (0..^3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 1 < 3))
85	45, 73, 46, 84	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ (0..^3)
86	85, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 ∈ (0..^(♯‘𝐹)))
87	86	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈ (0..^(♯‘𝐹)))
88		pthdadjvtx 28094	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
89		df-2 12036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 = (1 + 1)
90	89	fveq2i 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
91	90	neeq2i 3011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92	88, 91	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
93	69, 72, 87, 92	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
94		elfzo0 13426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ (0..^3) ↔ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 2 < 3))
95	50, 73, 51, 94	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (0..^3)
96	95, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → 2 ∈ (0..^(♯‘𝐹)))
97	96	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈ (0..^(♯‘𝐹)))
98		pthdadjvtx 28094	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
99	69, 72, 97, 98	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
100		neeq2 3009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
101		df-3 12037	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
102	101	fveq2i 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
103	102	neeq2i 3011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
104	100, 103	bitrdi 287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
105	104	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
106	105	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
107	99, 106	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
108	83, 93, 107	3jca 1127	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
109	108	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
110	109	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
111	110	impcom 408	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112		preq1 4675	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
113	112	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
114		preq2 4676	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
115	114	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
116	113, 115	3anbi13d 1437	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
117		neeq1 3008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
118		neeq2 3009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0)))
119	117, 118	3anbi13d 1437	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
120	116, 119	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
121		preq2 4676	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
122	121	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
123		preq1 4675	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
124	123	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
125	122, 124	3anbi12d 1436	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
126		neeq2 3009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
127		neeq1 3008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
128	126, 127	3anbi12d 1436	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
129	125, 128	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
130		preq2 4676	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
131	130	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
132		preq1 4675	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
133	132	eleq1d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
134	131, 133	3anbi23d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
135		neeq2 3009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
136		neeq1 3008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
137	135, 136	3anbi23d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
138	134, 137	anbi12d 631	. . . . . . . . . . . . . . 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 3575	. . . . . . . . . . . . . 14 ⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
140	61, 68, 111, 139	syl12anc 834	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))
141	140	ex 413	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
142	35, 141	sylbid 239	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
143	142	expd 416	. . . . . . . . . 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 414	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
147	146	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
148	147	expd 416	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))))
149	2, 148	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
150	149	imp 407	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
151	1, 150	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
152	151	3imp21 1113	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 ≠ wne 2945 ∀wral 3066 ∃wrex 3067 {cpr 4569 {ctp 4571 class class class wbr 5079 ⟶wf 6428 ‘cfv 6432 (class class class)co 7271 0cc0 10872 1c1 10873 + caddc 10875 < clt 11010 ℕcn 11973 2c2 12028 3c3 12029 ℕ₀cn0 12233 ...cfz 13238 ..^cfzo 13381 ♯chash 14042 Vtxcvtx 27364 Edgcedg 27415 UPGraphcupgr 27448 Walkscwlks 27961 Pathscpths 28076 Cyclesccycls 28149

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7582 ax-cnex 10928 ax-resscn 10929 ax-1cn 10930 ax-icn 10931 ax-addcl 10932 ax-addrcl 10933 ax-mulcl 10934 ax-mulrcl 10935 ax-mulcom 10936 ax-addass 10937 ax-mulass 10938 ax-distr 10939 ax-i2m1 10940 ax-1ne0 10941 ax-1rid 10942 ax-rnegex 10943 ax-rrecex 10944 ax-cnre 10945 ax-pre-lttri 10946 ax-pre-lttrn 10947 ax-pre-ltadd 10948 ax-pre-mulgt0 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ifp 1061 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4846 df-int 4886 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6201 df-ord 6268 df-on 6269 df-lim 6270 df-suc 6271 df-iota 6390 df-fun 6434 df-fn 6435 df-f 6436 df-f1 6437 df-fo 6438 df-f1o 6439 df-fv 6440 df-riota 7228 df-ov 7274 df-oprab 7275 df-mpo 7276 df-om 7707 df-1st 7824 df-2nd 7825 df-frecs 8088 df-wrecs 8119 df-recs 8193 df-rdg 8232 df-1o 8288 df-2o 8289 df-oadd 8292 df-er 8481 df-map 8600 df-pm 8601 df-en 8717 df-dom 8718 df-sdom 8719 df-fin 8720 df-dju 9660 df-card 9698 df-pnf 11012 df-mnf 11013 df-xr 11014 df-ltxr 11015 df-le 11016 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-xnn0 12306 df-z 12320 df-uz 12582 df-fz 13239 df-fzo 13382 df-hash 14043 df-word 14216 df-edg 27416 df-uhgr 27426 df-upgr 27450 df-wlks 27964 df-trls 28057 df-pths 28080 df-cycls 28151

This theorem is referenced by: umgr3v3e3cycl 28544

W3C validator