upgr4cycl4dv4e - Metamath Proof Explorer

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

Theorem upgr4cycl4dv4e 30270

Description: If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.)

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

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

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

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

Step	Hyp	Ref	Expression
1		cyclprop 29876	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 29808	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr4cycl4dv4e.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 29728	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (𝑃‘(♯‘𝐹)) = (𝑃‘4))
6	5	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
7	6	anbi2d 631	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = (0..^4))
9		fzo0to42pr 13699	. . . . . . . . . . . . . . . 16 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
10	8, 9	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = ({0, 1} ∪ {2, 3}))
11	10	raleqdv 3296	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		ralunb 4138	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13		c0ex 11129	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
14		1ex 11131	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
15		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 12290	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 12292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26	13, 14, 18, 25	ralpr 4645	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
27		2ex 12249	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ V
28		3ex 12254	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ V
29		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 7367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 12309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
32	30, 31	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3))
37		oveq1 7367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
38		3p1e4 12312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 + 1) = 4
39	37, 38	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 3 → (𝑘 + 1) = 4)
40	39	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
41	36, 40	preq12d 4686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
42	41	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
43	27, 28, 35, 42	ralpr 4645	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
44	26, 43	anbi12i 629	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
45	12, 44	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
46	11, 45	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
47	7, 46	anbi12d 633	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
48		preq2 4679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
49	48	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
50	49	eqcoms 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
51	50	anbi2d 631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
52	51	anbi2d 631	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
53	52	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
54		4nn0 12447	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ₀)
56		upgr4cycl4dv4e.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 29700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58		oveq2 7368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) = 4 → (0...(♯‘𝐹)) = (0...4))
59	58	feq2d 6646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 4 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉))
60	59	biimpcd 249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
61	2, 57, 60	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
62	61	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
63		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℕ₀)
64		0nn0 12443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ₀
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 ∈ ℕ₀)
66		4pos 12279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 4
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 < 4)
68	63, 65, 67	3jca 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4))
69		fvffz0 13591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
70	68, 69	sylan 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
71	70	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
72		1nn0 12444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 ∈ ℕ₀)
74		1lt4 12343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 4
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 < 4)
76	63, 73, 75	3jca 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4))
77		fvffz0 13591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
78	76, 77	sylan 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
79	78	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
80		2nn0 12445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ₀
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 ∈ ℕ₀)
82		2lt4 12342	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 < 4)
84	63, 81, 83	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4))
85		fvffz0 13591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
86	84, 85	sylan 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
87	86	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
88		3nn0 12446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ₀
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 ∈ ℕ₀)
90		3lt4 12341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 < 4
91	90	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 < 4)
92	63, 89, 91	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4))
93		fvffz0 13591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
94	92, 93	sylan 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
95	94	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
96		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
97		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
98		breq2 5090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝐹) = 4 → (1 < (♯‘𝐹) ↔ 1 < 4))
99	74, 98	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝐹) = 4 → 1 < (♯‘𝐹))
100	99	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 1 < (♯‘𝐹))
101		simpll 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (♯‘𝐹) = 4)
102	8	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (0..^(♯‘𝐹)) = (0..^4))
103		4nn 12255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 4 ∈ ℕ
104		lbfzo0 13645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
105	103, 104	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ (0..^4)
106		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^4)))
107	105, 106	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 0 ∈ (0..^(♯‘𝐹)))
108	107	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 0 ∈ (0..^(♯‘𝐹)))
109		pthdadjvtx 29811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
110	108, 109	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
111		1e0p1 12677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 = (0 + 1)
112	111	fveq2i 6837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
113	112	neeq2i 2998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114	110, 113	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
115		simp1 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
116		elfzo0 13646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ∈ (0..^4) ↔ (2 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 2 < 4))
117	80, 103, 82, 116	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ (0..^4)
118		2ne0 12276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ≠ 0
119		fzo1fzo0n0 13661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
120	117, 118, 119	mpbir2an 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ (1..^4)
121		oveq2 7368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐹) = 4 → (1..^(♯‘𝐹)) = (1..^4))
122	120, 121	eleqtrrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ∈ (1..^(♯‘𝐹)))
123		0elfz 13569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 ∈ ℕ₀ → 0 ∈ (0...4))
124	54, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ (0...4)
125	124, 58	eleqtrrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 0 ∈ (0...(♯‘𝐹)))
126	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ≠ 0)
127	122, 125, 126	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
128	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
129	128	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
130		pthdivtx 29810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
131	115, 129, 130	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
132	131	necomd 2988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
133		elfzo0 13646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
134	88, 103, 90, 133	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ (0..^4)
135		3ne0 12278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ≠ 0
136		fzo1fzo0n0 13661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
137	134, 135, 136	mpbir2an 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ∈ (1..^4)
138	137, 121	eleqtrrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (1..^(♯‘𝐹)))
139	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ≠ 0)
140	138, 125, 139	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
142	141	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
143		pthdivtx 29810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
144	115, 142, 143	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
145	144	necomd 2988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
146	114, 132, 145	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
147		elfzo0 13646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
148	72, 103, 74, 147	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ (0..^4)
149		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈ (0..^4)))
150	148, 149	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 1 ∈ (0..^(♯‘𝐹)))
151	150	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 1 ∈ (0..^(♯‘𝐹)))
152		pthdadjvtx 29811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
153	151, 152	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
154		df-2 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 = (1 + 1)
155	154	fveq2i 6837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
156	155	neeq2i 2998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157	153, 156	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
158		ax-1ne0 11098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
159		fzo1fzo0n0 13661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
160	148, 158, 159	mpbir2an 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ (1..^4)
161	160, 121	eleqtrrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ∈ (1..^(♯‘𝐹)))
162		3re 12252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ ℝ
163		4re 12256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 4 ∈ ℝ
164	162, 163, 90	ltleii 11260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ≤ 4
165		elfz2nn0 13563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (3 ∈ (0...4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀ ∧ 3 ≤ 4))
166	88, 54, 164, 165	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ∈ (0...4)
167	166, 58	eleqtrrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (0...(♯‘𝐹)))
168		1re 11135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ∈ ℝ
169		1lt3 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 3
170	168, 169	ltneii 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ≠ 3
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ≠ 3)
172	161, 167, 171	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐹) = 4 → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
173	172	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
174	173	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
175		pthdivtx 29810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
176	115, 174, 175	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
177		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (2 ∈ (0..^(♯‘𝐹)) ↔ 2 ∈ (0..^4)))
178	117, 177	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 2 ∈ (0..^(♯‘𝐹)))
179	178	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 2 ∈ (0..^(♯‘𝐹)))
180		pthdadjvtx 29811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
181	179, 180	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
182		df-3 12236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 3 = (2 + 1)
183	182	fveq2i 6837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
184	183	neeq2i 2998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185	181, 184	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
186	157, 176, 185	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
187	146, 186	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
188	97, 100, 101, 102, 187	syl112anc 1377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
190		preq2 4679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
191	190	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
192	191	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
193		preq1 4678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
194	193	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
195	194	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
196	192, 195	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
197		neeq2 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
198	197	3anbi2d 1444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
199		neeq2 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
200		neeq1 2995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑))
201	199, 200	3anbi13d 1441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
202	198, 201	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
203	196, 202	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = (𝑃‘2) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))))
204		preq2 4679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
205	204	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
206		preq1 4678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
207	206	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
208	205, 207	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
209	208	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
210		neeq2 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
211	210	3anbi3d 1445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
212		neeq2 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
213		neeq2 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
214	212, 213	3anbi23d 1442	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
215	211, 214	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = (𝑃‘3) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))))
216	209, 215	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑃‘3) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))))
217	203, 216	rspc2ev 3578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃‘2) ∈ 𝑉 ∧ (𝑃‘3) ∈ 𝑉 ∧ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
218	87, 95, 96, 189, 217	syl112anc 1377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
219	71, 79, 218	3jca 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
220	219	exp31 419	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
221	55, 62, 220	mp2and 700	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
222	221	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
223	53, 222	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
224	223	exp31 419	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
225	224	imp4c 423	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
226		preq1 4678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
227	226	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
228	227	anbi1d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
229		preq2 4679	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
230	229	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
231	230	anbi2d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
232	228, 231	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
233		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
234		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐))
235		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑))
236	233, 234, 235	3anbi123d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
237	236	anbi1d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
238	232, 237	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
239	238	2rexbidv 3203	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
240		preq2 4679	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
241	240	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
242		preq1 4678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
243	242	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
244	241, 243	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
245	244	anbi1d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
246		neeq2 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
247	246	3anbi1d 1443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
248		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
249		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑))
250	248, 249	3anbi12d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))
251	247, 250	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
252	245, 251	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
253	252	2rexbidv 3203	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
254	239, 253	rspc2ev 3578	. . . . . . . . . . . . 13 ⊢ (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
255	225, 254	syl6 35	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
256	47, 255	sylbid 240	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
257	256	expd 415	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
258	257	com13 88	. . . . . . . . 9 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
259	4, 258	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
260	259	expcom 413	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
261	260	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
262	261	expd 415	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
263	2, 262	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
264	263	imp 406	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
265	1, 264	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
266	265	3imp21 1114	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∪ cun 3888 {cpr 4570 class class class wbr 5086 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 0cc0 11029 1c1 11030 + caddc 11032 < clt 11170 ≤ cle 11171 ℕcn 12165 2c2 12227 3c3 12228 4c4 12229 ℕ₀cn0 12428 ...cfz 13452 ..^cfzo 13599 ♯chash 14283 Vtxcvtx 29079 Edgcedg 29130 UPGraphcupgr 29163 Walkscwlks 29680 Pathscpths 29793 Cyclesccycls 29868

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

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 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-oadd 8402 df-er 8636 df-map 8768 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-fzo 13600 df-hash 14284 df-word 14467 df-edg 29131 df-uhgr 29141 df-upgr 29165 df-wlks 29683 df-trls 29774 df-pths 29797 df-cycls 29870

This theorem is referenced by: n4cyclfrgr 30376 pgn4cyclex 48614

W3C validator