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 27729

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 27297	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 27231	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr4cycl4dv4e.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 27144	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6496	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (𝑃‘(♯‘𝐹)) = (𝑃‘4))
6	5	eqeq2d 2781	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
7	6	anbi2d 620	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8		oveq2 6982	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = (0..^4))
9		fzo0to42pr 12937	. . . . . . . . . . . . . . . 16 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
10	8, 9	syl6eq 2823	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = ({0, 1} ∪ {2, 3}))
11	10	raleqdv 3348	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		ralunb 4049	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13		c0ex 10431	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
14		1ex 10433	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
15		fveq2 6496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 11568	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 11570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
22	20, 21	syl6eq 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26	13, 14, 18, 25	ralpr 4506	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
27		2ex 11515	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ V
28		3ex 11521	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ V
29		fveq2 6496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 11587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
32	30, 31	syl6eq 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36		fveq2 6496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3))
37		oveq1 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
38		3p1e4 11590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 + 1) = 4
39	37, 38	syl6eq 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 3 → (𝑘 + 1) = 4)
40	39	fveq2d 6500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
41	36, 40	preq12d 4547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
42	41	eleq1d 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
43	27, 28, 35, 42	ralpr 4506	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
44	26, 43	anbi12i 618	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
45	12, 44	bitri 267	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
46	11, 45	syl6bb 279	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
47	7, 46	anbi12d 622	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
48		preq2 4540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
49	48	eleq1d 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
50	49	eqcoms 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
51	50	anbi2d 620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
52	51	anbi2d 620	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
53	52	adantl 474	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
54		4nn0 11726	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ₀)
56		upgr4cycl4dv4e.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 27116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58		oveq2 6982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) = 4 → (0...(♯‘𝐹)) = (0...4))
59	58	feq2d 6327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 4 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉))
60	59	biimpcd 241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
61	2, 57, 60	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
62	61	impcom 399	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
63		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℕ₀)
64		0nn0 11722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ₀
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 ∈ ℕ₀)
66		4pos 11552	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 4
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 < 4)
68	63, 65, 67	3jca 1109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4))
69		fvffz0 12839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
70	68, 69	sylan 572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
71	70	ad2antlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
72		1nn0 11723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 ∈ ℕ₀)
74		1lt4 11621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 4
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 < 4)
76	63, 73, 75	3jca 1109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4))
77		fvffz0 12839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
78	76, 77	sylan 572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
79	78	ad2antlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
80		2nn0 11724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ₀
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 ∈ ℕ₀)
82		2lt4 11620	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 < 4)
84	63, 81, 83	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4))
85		fvffz0 12839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
86	84, 85	sylan 572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
87	86	ad2antlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
88		3nn0 11725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ₀
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 ∈ ℕ₀)
90		3lt4 11619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 < 4
91	90	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 < 4)
92	63, 89, 91	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4))
93		fvffz0 12839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
94	92, 93	sylan 572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
95	94	ad2antlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
96		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
97		simplr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
98		breq2 4929	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝐹) = 4 → (1 < (♯‘𝐹) ↔ 1 < 4))
99	74, 98	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝐹) = 4 → 1 < (♯‘𝐹))
100	99	ad2antrr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 1 < (♯‘𝐹))
101		simpll 755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (♯‘𝐹) = 4)
102	8	ad2antrr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (0..^(♯‘𝐹)) = (0..^4))
103		4nn 11522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 4 ∈ ℕ
104		lbfzo0 12890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
105	103, 104	mpbir 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ (0..^4)
106		eleq2 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^4)))
107	105, 106	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 0 ∈ (0..^(♯‘𝐹)))
108	107	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 0 ∈ (0..^(♯‘𝐹)))
109		pthdadjvtx 27234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
110	108, 109	syl3an3 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
111		1e0p1 11952	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 = (0 + 1)
112	111	fveq2i 6499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
113	112	neeq2i 3025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114	110, 113	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
115		simp1 1117	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
116		elfzo0 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ∈ (0..^4) ↔ (2 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 2 < 4))
117	80, 103, 82, 116	mpbir3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ (0..^4)
118		2ne0 11549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ≠ 0
119		fzo1fzo0n0 12901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
120	117, 118, 119	mpbir2an 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ (1..^4)
121		oveq2 6982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐹) = 4 → (1..^(♯‘𝐹)) = (1..^4))
122	120, 121	syl5eleqr 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ∈ (1..^(♯‘𝐹)))
123		0elfz 12818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 ∈ ℕ₀ → 0 ∈ (0...4))
124	54, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ (0...4)
125	124, 58	syl5eleqr 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 0 ∈ (0...(♯‘𝐹)))
126	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ≠ 0)
127	122, 125, 126	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
128	127	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
129	128	3ad2ant3 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
130		pthdivtx 27233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
131	115, 129, 130	syl2anc 576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
132	131	necomd 3015	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
133		elfzo0 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
134	88, 103, 90, 133	mpbir3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ (0..^4)
135		3ne0 11551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ≠ 0
136		fzo1fzo0n0 12901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
137	134, 135, 136	mpbir2an 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ∈ (1..^4)
138	137, 121	syl5eleqr 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (1..^(♯‘𝐹)))
139	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ≠ 0)
140	138, 125, 139	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
141	140	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
142	141	3ad2ant3 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
143		pthdivtx 27233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
144	115, 142, 143	syl2anc 576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
145	144	necomd 3015	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
146	114, 132, 145	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
147		elfzo0 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
148	72, 103, 74, 147	mpbir3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ (0..^4)
149		eleq2 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈ (0..^4)))
150	148, 149	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 1 ∈ (0..^(♯‘𝐹)))
151	150	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 1 ∈ (0..^(♯‘𝐹)))
152		pthdadjvtx 27234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
153	151, 152	syl3an3 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
154		df-2 11501	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 = (1 + 1)
155	154	fveq2i 6499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
156	155	neeq2i 3025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157	153, 156	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
158		ax-1ne0 10402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
159		fzo1fzo0n0 12901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
160	148, 158, 159	mpbir2an 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ (1..^4)
161	160, 121	syl5eleqr 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ∈ (1..^(♯‘𝐹)))
162		3re 11518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ ℝ
163		4re 11523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 4 ∈ ℝ
164	162, 163, 90	ltleii 10561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ≤ 4
165		elfz2nn0 12812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (3 ∈ (0...4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀ ∧ 3 ≤ 4))
166	88, 54, 164, 165	mpbir3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ∈ (0...4)
167	166, 58	syl5eleqr 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (0...(♯‘𝐹)))
168		1re 10437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ∈ ℝ
169		1lt3 11618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 3
170	168, 169	ltneii 10551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ≠ 3
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ≠ 3)
172	161, 167, 171	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐹) = 4 → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
173	172	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
174	173	3ad2ant3 1116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
175		pthdivtx 27233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
176	115, 174, 175	syl2anc 576	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
177		eleq2 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (2 ∈ (0..^(♯‘𝐹)) ↔ 2 ∈ (0..^4)))
178	117, 177	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 2 ∈ (0..^(♯‘𝐹)))
179	178	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 2 ∈ (0..^(♯‘𝐹)))
180		pthdadjvtx 27234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
181	179, 180	syl3an3 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
182		df-3 11502	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 3 = (2 + 1)
183	182	fveq2i 6499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
184	183	neeq2i 3025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185	181, 184	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
186	157, 176, 185	3jca 1109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
187	146, 186	jca 504	. . . . . . . . . . . . . . . . . . . . . . 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 1355	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
189	188	adantr 473	. . . . . . . . . . . . . . . . . . . . 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 4540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
191	190	eleq1d 2843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
192	191	anbi2d 620	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
193		preq1 4539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
194	193	eleq1d 2843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
195	194	anbi1d 621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
196	192, 195	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
197		neeq2 3023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
198	197	3anbi2d 1421	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
199		neeq2 3023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
200		neeq1 3022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑))
201	199, 200	3anbi13d 1418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
202	198, 201	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
203	196, 202	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . 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 4540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
205	204	eleq1d 2843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
206		preq1 4539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
207	206	eleq1d 2843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
208	205, 207	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
209	208	anbi2d 620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
210		neeq2 3023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
211	210	3anbi3d 1422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
212		neeq2 3023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
213		neeq2 3023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
214	212, 213	3anbi23d 1419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
215	211, 214	anbi12d 622	. . . . . . . . . . . . . . . . . . . . . . 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 622	. . . . . . . . . . . . . . . . . . . . . 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 3543	. . . . . . . . . . . . . . . . . . . . 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 1355	. . . . . . . . . . . . . . . . . . . 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 1109	. . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . 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 687	. . . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . 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 416	. . . . . . . . . . . . 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 4539	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
227	226	eleq1d 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
228	227	anbi1d 621	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
229		preq2 4540	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
230	229	eleq1d 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
231	230	anbi2d 620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
232	228, 231	anbi12d 622	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
233		neeq1 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
234		neeq1 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐))
235		neeq1 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑))
236	233, 234, 235	3anbi123d 1416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
237	236	anbi1d 621	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
238	232, 237	anbi12d 622	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
239	238	2rexbidv 3238	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
240		preq2 4540	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
241	240	eleq1d 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
242		preq1 4539	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
243	242	eleq1d 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
244	241, 243	anbi12d 622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
245	244	anbi1d 621	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
246		neeq2 3023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
247	246	3anbi1d 1420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
248		neeq1 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
249		neeq1 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑))
250	248, 249	3anbi12d 1417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))
251	247, 250	anbi12d 622	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
252	245, 251	anbi12d 622	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
253	252	2rexbidv 3238	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
254	239, 253	rspc2ev 3543	. . . . . . . . . . . . 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 232	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
257	256	expd 408	. . . . . . . . . 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 406	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
261	260	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
262	261	expd 408	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
263	2, 262	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
264	263	imp 398	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
265	1, 264	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
266	265	3imp21 1095	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1069 = wceq 1508 ∈ wcel 2051 ≠ wne 2960 ∀wral 3081 ∃wrex 3082 ∪ cun 3820 {cpr 4437 class class class wbr 4925 ⟶wf 6181 ‘cfv 6185 (class class class)co 6974 0cc0 10333 1c1 10334 + caddc 10336 < clt 10472 ≤ cle 10473 ℕcn 11437 2c2 11493 3c3 11494 4c4 11495 ℕ₀cn0 11705 ...cfz 12706 ..^cfzo 12847 ♯chash 13503 Vtxcvtx 26499 Edgcedg 26550 UPGraphcupgr 26583 Walkscwlks 27096 Pathscpths 27216 Cyclesccycls 27289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-cnex 10389 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 ax-pre-mulgt0 10410

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-ifp 1045 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-int 4746 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-1st 7499 df-2nd 7500 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-2o 7904 df-oadd 7907 df-er 8087 df-map 8206 df-pm 8207 df-en 8305 df-dom 8306 df-sdom 8307 df-fin 8308 df-dju 9122 df-card 9160 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-sub 10670 df-neg 10671 df-nn 11438 df-2 11501 df-3 11502 df-4 11503 df-n0 11706 df-xnn0 11778 df-z 11792 df-uz 12057 df-fz 12707 df-fzo 12848 df-hash 13504 df-word 13671 df-edg 26551 df-uhgr 26561 df-upgr 26585 df-wlks 27099 df-trls 27195 df-pths 27220 df-cycls 27291

This theorem is referenced by: n4cyclfrgr 27840

W3C validator