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 28549

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 28161	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 28095	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr4cycl4dv4e.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 28012	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (𝑃‘(♯‘𝐹)) = (𝑃‘4))
6	5	eqeq2d 2749	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
7	6	anbi2d 629	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8		oveq2 7283	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = (0..^4))
9		fzo0to42pr 13474	. . . . . . . . . . . . . . . 16 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
10	8, 9	eqtrdi 2794	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = ({0, 1} ∪ {2, 3}))
11	10	raleqdv 3348	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		ralunb 4125	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13		c0ex 10969	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
14		1ex 10971	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
15		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 12096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 12098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26	13, 14, 18, 25	ralpr 4636	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
27		2ex 12050	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ V
28		3ex 12055	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ V
29		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 7282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 12115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
32	30, 31	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3))
37		oveq1 7282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
38		3p1e4 12118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 + 1) = 4
39	37, 38	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 3 → (𝑘 + 1) = 4)
40	39	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
41	36, 40	preq12d 4677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
42	41	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
43	27, 28, 35, 42	ralpr 4636	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
44	26, 43	anbi12i 627	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
45	12, 44	bitri 274	. . . . . . . . . . . . . 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 631	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
48		preq2 4670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
49	48	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
50	49	eqcoms 2746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
51	50	anbi2d 629	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
52	51	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
53	52	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
54		4nn0 12252	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ₀)
56		upgr4cycl4dv4e.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 27983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) = 4 → (0...(♯‘𝐹)) = (0...4))
59	58	feq2d 6586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 4 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉))
60	59	biimpcd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
61	2, 57, 60	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
62	61	impcom 408	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
63		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℕ₀)
64		0nn0 12248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ₀
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 ∈ ℕ₀)
66		4pos 12080	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 4
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 < 4)
68	63, 65, 67	3jca 1127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4))
69		fvffz0 13374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
70	68, 69	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
71	70	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
72		1nn0 12249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 ∈ ℕ₀)
74		1lt4 12149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 4
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 < 4)
76	63, 73, 75	3jca 1127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4))
77		fvffz0 13374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
78	76, 77	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
79	78	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
80		2nn0 12250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ₀
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 ∈ ℕ₀)
82		2lt4 12148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 < 4)
84	63, 81, 83	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4))
85		fvffz0 13374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
86	84, 85	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
87	86	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
88		3nn0 12251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ₀
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 ∈ ℕ₀)
90		3lt4 12147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 < 4
91	90	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 < 4)
92	63, 89, 91	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4))
93		fvffz0 13374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
94	92, 93	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
95	94	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
96		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
97		simplr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
98		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝐹) = 4 → (1 < (♯‘𝐹) ↔ 1 < 4))
99	74, 98	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝐹) = 4 → 1 < (♯‘𝐹))
100	99	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 1 < (♯‘𝐹))
101		simpll 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (♯‘𝐹) = 4)
102	8	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (0..^(♯‘𝐹)) = (0..^4))
103		4nn 12056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 4 ∈ ℕ
104		lbfzo0 13427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
105	103, 104	mpbir 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ (0..^4)
106		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^4)))
107	105, 106	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 0 ∈ (0..^(♯‘𝐹)))
108	107	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 0 ∈ (0..^(♯‘𝐹)))
109		pthdadjvtx 28098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
110	108, 109	syl3an3 1164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
111		1e0p1 12479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 = (0 + 1)
112	111	fveq2i 6777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
113	112	neeq2i 3009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114	110, 113	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
115		simp1 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
116		elfzo0 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ∈ (0..^4) ↔ (2 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 2 < 4))
117	80, 103, 82, 116	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ (0..^4)
118		2ne0 12077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ≠ 0
119		fzo1fzo0n0 13438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
120	117, 118, 119	mpbir2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ (1..^4)
121		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐹) = 4 → (1..^(♯‘𝐹)) = (1..^4))
122	120, 121	eleqtrrid 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ∈ (1..^(♯‘𝐹)))
123		0elfz 13353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 ∈ ℕ₀ → 0 ∈ (0...4))
124	54, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ (0...4)
125	124, 58	eleqtrrid 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 0 ∈ (0...(♯‘𝐹)))
126	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ≠ 0)
127	122, 125, 126	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
128	127	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
129	128	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
130		pthdivtx 28097	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
131	115, 129, 130	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
132	131	necomd 2999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
133		elfzo0 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
134	88, 103, 90, 133	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ (0..^4)
135		3ne0 12079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ≠ 0
136		fzo1fzo0n0 13438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
137	134, 135, 136	mpbir2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ∈ (1..^4)
138	137, 121	eleqtrrid 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (1..^(♯‘𝐹)))
139	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ≠ 0)
140	138, 125, 139	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
141	140	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
142	141	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
143		pthdivtx 28097	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
144	115, 142, 143	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
145	144	necomd 2999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
146	114, 132, 145	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
147		elfzo0 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
148	72, 103, 74, 147	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ (0..^4)
149		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈ (0..^4)))
150	148, 149	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 1 ∈ (0..^(♯‘𝐹)))
151	150	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 1 ∈ (0..^(♯‘𝐹)))
152		pthdadjvtx 28098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
153	151, 152	syl3an3 1164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
154		df-2 12036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 = (1 + 1)
155	154	fveq2i 6777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
156	155	neeq2i 3009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157	153, 156	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
158		ax-1ne0 10940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
159		fzo1fzo0n0 13438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
160	148, 158, 159	mpbir2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ (1..^4)
161	160, 121	eleqtrrid 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ∈ (1..^(♯‘𝐹)))
162		3re 12053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ ℝ
163		4re 12057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 4 ∈ ℝ
164	162, 163, 90	ltleii 11098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ≤ 4
165		elfz2nn0 13347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (3 ∈ (0...4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀ ∧ 3 ≤ 4))
166	88, 54, 164, 165	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ∈ (0...4)
167	166, 58	eleqtrrid 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (0...(♯‘𝐹)))
168		1re 10975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ∈ ℝ
169		1lt3 12146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 3
170	168, 169	ltneii 11088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ≠ 3
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ≠ 3)
172	161, 167, 171	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐹) = 4 → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
173	172	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
174	173	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
175		pthdivtx 28097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
176	115, 174, 175	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
177		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (2 ∈ (0..^(♯‘𝐹)) ↔ 2 ∈ (0..^4)))
178	117, 177	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 2 ∈ (0..^(♯‘𝐹)))
179	178	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 2 ∈ (0..^(♯‘𝐹)))
180		pthdadjvtx 28098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
181	179, 180	syl3an3 1164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
182		df-3 12037	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 3 = (2 + 1)
183	182	fveq2i 6777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
184	183	neeq2i 3009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185	181, 184	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
186	157, 176, 185	3jca 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
187	146, 186	jca 512	. . . . . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
189	188	adantr 481	. . . . . . . . . . . . . . . . . . . . 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 4670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
191	190	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
192	191	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
193		preq1 4669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
194	193	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
195	194	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
196	192, 195	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
197		neeq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
198	197	3anbi2d 1440	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
199		neeq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
200		neeq1 3006	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑))
201	199, 200	3anbi13d 1437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
202	198, 201	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
203	196, 202	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 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 4670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
205	204	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
206		preq1 4669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
207	206	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
208	205, 207	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
209	208	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
210		neeq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
211	210	3anbi3d 1441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
212		neeq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
213		neeq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
214	212, 213	3anbi23d 1438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
215	211, 214	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 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 631	. . . . . . . . . . . . . . . . . . . . . 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 3572	. . . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . . . 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 1127	. . . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . . . . . 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 696	. . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . 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 239	. . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . 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 424	. . . . . . . . . . . . 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 4669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
227	226	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
228	227	anbi1d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
229		preq2 4670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
230	229	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
231	230	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
232	228, 231	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
233		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
234		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐))
235		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑))
236	233, 234, 235	3anbi123d 1435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
237	236	anbi1d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
238	232, 237	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
239	238	2rexbidv 3229	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
240		preq2 4670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
241	240	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
242		preq1 4669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
243	242	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
244	241, 243	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
245	244	anbi1d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
246		neeq2 3007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
247	246	3anbi1d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
248		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
249		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑))
250	248, 249	3anbi12d 1436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))
251	247, 250	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
252	245, 251	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
253	252	2rexbidv 3229	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
254	239, 253	rspc2ev 3572	. . . . . . . . . . . . 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 239	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
257	256	expd 416	. . . . . . . . . 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 414	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
261	260	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
262	261	expd 416	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
263	2, 262	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
264	263	imp 407	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
265	1, 264	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
266	265	3imp21 1113	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 ∪ cun 3885 {cpr 4563 class class class wbr 5074 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 0cc0 10871 1c1 10872 + caddc 10874 < clt 11009 ≤ cle 11010 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 ℕ₀cn0 12233 ...cfz 13239 ..^cfzo 13382 ♯chash 14044 Vtxcvtx 27366 Edgcedg 27417 UPGraphcupgr 27450 Walkscwlks 27963 Pathscpths 28080 Cyclesccycls 28153

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

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 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-oadd 8301 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-n0 12234 df-xnn0 12306 df-z 12320 df-uz 12583 df-fz 13240 df-fzo 13383 df-hash 14045 df-word 14218 df-edg 27418 df-uhgr 27428 df-upgr 27452 df-wlks 27966 df-trls 28060 df-pths 28084 df-cycls 28155

This theorem is referenced by: n4cyclfrgr 28655

W3C validator