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 30199

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 29813	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 29745	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr3v3e3cycl.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 29663	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3))
6	5	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
7	6	anbi2d 630	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8		oveq2 7439	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = (0..^3))
9		fzo0to3tp 13791	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) = {0, 1, 2}
10	8, 9	eqtrdi 2793	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = {0, 1, 2})
11	10	raleqdv 3326	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		c0ex 11255	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
13		1ex 11257	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
14		2ex 12343	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ V
15		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 12389	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4741	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 12391	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4741	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
27		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
28		2p1e3 12408	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 + 1) = 3
29	27, 28	eqtrdi 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
30	29	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
31	26, 30	preq12d 4741	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
32	31	eleq1d 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
33	12, 13, 14, 18, 25, 32	raltp 4705	. . . . . . . . . . . . . 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 632	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
36		upgr3v3e3cycl.v	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 = (Vtx‘𝐺)
37	36	wlkp 29634	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
38		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (0...(♯‘𝐹)) = (0...3))
39	38	feq2d 6722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉))
40		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉)
41		3nn0 12544	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℕ₀
42		0elfz 13664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 ∈ ℕ₀ → 0 ∈ (0...3))
43	41, 42	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
44	40, 43	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
45		1nn0 12542	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℕ₀
46		1lt3 12439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < 3
47		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
48	47	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
49	41, 45, 46, 48	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
50		2nn0 12543	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℕ₀
51		2lt3 12438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 < 3
52		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
53	52	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
54	41, 50, 51, 53	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
55	44, 49, 54	3jca 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
56	39, 55	biimtrdi 253	. . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
60	59	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
61	60	impcom 407	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
62		preq2 4734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
63	62	eqcoms 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
64	63	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
65	64	eleq1d 2826	. . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
68	67	adantl 481	. . . . . . . . . . . . . 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 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → (1 < (♯‘𝐹) ↔ 1 < 3))
71	46, 70	mpbiri 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 < (♯‘𝐹))
72	71	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 < (♯‘𝐹))
73		3nn 12345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℕ
74		lbfzo0 13739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
75	73, 74	mpbir 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ (0..^3)
76	75, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 0 ∈ (0..^(♯‘𝐹)))
77	76	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈ (0..^(♯‘𝐹)))
78		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
79		1e0p1 12775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 = (0 + 1)
80	79	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
81	80	neeq2i 3006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82	78, 81	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
83	69, 72, 77, 82	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
84		elfzo0 13740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ (0..^3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 1 < 3))
85	45, 73, 46, 84	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ (0..^3)
86	85, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) = 3 → 1 ∈ (0..^(♯‘𝐹)))
87	86	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈ (0..^(♯‘𝐹)))
88		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
89		df-2 12329	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 = (1 + 1)
90	89	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
91	90	neeq2i 3006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92	88, 91	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
93	69, 72, 87, 92	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
94		elfzo0 13740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ (0..^3) ↔ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ ∧ 2 < 3))
95	50, 73, 51, 94	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (0..^3)
96	95, 8	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 3 → 2 ∈ (0..^(♯‘𝐹)))
97	96	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈ (0..^(♯‘𝐹)))
98		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . 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 3004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
101		df-3 12330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
102	101	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
103	102	neeq2i 3006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
104	100, 103	bitrdi 287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
105	104	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
106	105	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
107	99, 106	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
108	83, 93, 107	3jca 1129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
109	108	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
110	109	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
111	110	impcom 407	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112		preq1 4733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
113	112	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
114		preq2 4734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
115	114	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
116	113, 115	3anbi13d 1440	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
117		neeq1 3003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
118		neeq2 3004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0)))
119	117, 118	3anbi13d 1440	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
120	116, 119	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
121		preq2 4734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
122	121	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
123		preq1 4733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
124	123	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
125	122, 124	3anbi12d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
126		neeq2 3004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
127		neeq1 3003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
128	126, 127	3anbi12d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))
129	125, 128	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))))
130		preq2 4734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
131	130	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
132		preq1 4733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
133	132	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
134	131, 133	3anbi23d 1441	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
135		neeq2 3004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
136		neeq1 3003	. . . . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . 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 412	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
142	35, 141	sylbid 240	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))
143	142	expd 415	. . . . . . . . . 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 413	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
147	146	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
148	147	expd 415	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))))
149	2, 148	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))
150	149	imp 406	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
151	1, 150	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))
152	151	3imp21 1114	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {cpr 4628 {ctp 4630 class class class wbr 5143 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 0cc0 11155 1c1 11156 + caddc 11158 < clt 11295 ℕcn 12266 2c2 12321 3c3 12322 ℕ₀cn0 12526 ...cfz 13547 ..^cfzo 13694 ♯chash 14369 Vtxcvtx 29013 Edgcedg 29064 UPGraphcupgr 29097 Walkscwlks 29614 Pathscpths 29730 Cyclesccycls 29805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ifp 1064 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-fz 13548 df-fzo 13695 df-hash 14370 df-word 14553 df-edg 29065 df-uhgr 29075 df-upgr 29099 df-wlks 29617 df-trls 29710 df-pths 29734 df-cycls 29807

This theorem is referenced by: umgr3v3e3cycl 30203

W3C validator