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 27966

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 27576	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 27510	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr4cycl4dv4e.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 27428	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6672	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (𝑃‘(♯‘𝐹)) = (𝑃‘4))
6	5	eqeq2d 2834	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
7	6	anbi2d 630	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8		oveq2 7166	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = (0..^4))
9		fzo0to42pr 13127	. . . . . . . . . . . . . . . 16 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
10	8, 9	syl6eq 2874	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = ({0, 1} ∪ {2, 3}))
11	10	raleqdv 3417	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		ralunb 4169	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13		c0ex 10637	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
14		1ex 10639	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
15		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 11763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 11765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
22	20, 21	syl6eq 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26	13, 14, 18, 25	ralpr 4638	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
27		2ex 11717	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ V
28		3ex 11722	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ V
29		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 11782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
32	30, 31	syl6eq 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3))
37		oveq1 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
38		3p1e4 11785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 + 1) = 4
39	37, 38	syl6eq 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 3 → (𝑘 + 1) = 4)
40	39	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
41	36, 40	preq12d 4679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
42	41	eleq1d 2899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
43	27, 28, 35, 42	ralpr 4638	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
44	26, 43	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
45	12, 44	bitri 277	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
46	11, 45	syl6bb 289	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
47	7, 46	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
48		preq2 4672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
49	48	eleq1d 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
50	49	eqcoms 2831	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
51	50	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
52	51	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
53	52	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
54		4nn0 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ₀)
56		upgr4cycl4dv4e.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 27400	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58		oveq2 7166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) = 4 → (0...(♯‘𝐹)) = (0...4))
59	58	feq2d 6502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 4 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉))
60	59	biimpcd 251	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
61	2, 57, 60	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
62	61	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
63		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℕ₀)
64		0nn0 11915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ₀
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 ∈ ℕ₀)
66		4pos 11747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 4
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 < 4)
68	63, 65, 67	3jca 1124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4))
69		fvffz0 13028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
70	68, 69	sylan 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
71	70	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
72		1nn0 11916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 ∈ ℕ₀)
74		1lt4 11816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 4
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 < 4)
76	63, 73, 75	3jca 1124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4))
77		fvffz0 13028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
78	76, 77	sylan 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
79	78	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
80		2nn0 11917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ₀
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 ∈ ℕ₀)
82		2lt4 11815	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 < 4)
84	63, 81, 83	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4))
85		fvffz0 13028	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
86	84, 85	sylan 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
87	86	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
88		3nn0 11918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ₀
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 ∈ ℕ₀)
90		3lt4 11814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 < 4
91	90	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 < 4)
92	63, 89, 91	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4))
93		fvffz0 13028	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
94	92, 93	sylan 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
95	94	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
96		simpr 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
97		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
98		breq2 5072	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝐹) = 4 → (1 < (♯‘𝐹) ↔ 1 < 4))
99	74, 98	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝐹) = 4 → 1 < (♯‘𝐹))
100	99	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 1 < (♯‘𝐹))
101		simpll 765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (♯‘𝐹) = 4)
102	8	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (0..^(♯‘𝐹)) = (0..^4))
103		4nn 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 4 ∈ ℕ
104		lbfzo0 13080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
105	103, 104	mpbir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ (0..^4)
106		eleq2 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^4)))
107	105, 106	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 0 ∈ (0..^(♯‘𝐹)))
108	107	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 0 ∈ (0..^(♯‘𝐹)))
109		pthdadjvtx 27513	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
110	108, 109	syl3an3 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
111		1e0p1 12143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 = (0 + 1)
112	111	fveq2i 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
113	112	neeq2i 3083	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114	110, 113	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
115		simp1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
116		elfzo0 13081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ∈ (0..^4) ↔ (2 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 2 < 4))
117	80, 103, 82, 116	mpbir3an 1337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ (0..^4)
118		2ne0 11744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ≠ 0
119		fzo1fzo0n0 13091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
120	117, 118, 119	mpbir2an 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ (1..^4)
121		oveq2 7166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐹) = 4 → (1..^(♯‘𝐹)) = (1..^4))
122	120, 121	eleqtrrid 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ∈ (1..^(♯‘𝐹)))
123		0elfz 13007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 ∈ ℕ₀ → 0 ∈ (0...4))
124	54, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ (0...4)
125	124, 58	eleqtrrid 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 0 ∈ (0...(♯‘𝐹)))
126	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ≠ 0)
127	122, 125, 126	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
128	127	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
129	128	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
130		pthdivtx 27512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
131	115, 129, 130	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
132	131	necomd 3073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
133		elfzo0 13081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
134	88, 103, 90, 133	mpbir3an 1337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ (0..^4)
135		3ne0 11746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ≠ 0
136		fzo1fzo0n0 13091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
137	134, 135, 136	mpbir2an 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ∈ (1..^4)
138	137, 121	eleqtrrid 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (1..^(♯‘𝐹)))
139	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ≠ 0)
140	138, 125, 139	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
141	140	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
142	141	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
143		pthdivtx 27512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
144	115, 142, 143	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
145	144	necomd 3073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
146	114, 132, 145	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
147		elfzo0 13081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
148	72, 103, 74, 147	mpbir3an 1337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ (0..^4)
149		eleq2 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈ (0..^4)))
150	148, 149	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 1 ∈ (0..^(♯‘𝐹)))
151	150	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 1 ∈ (0..^(♯‘𝐹)))
152		pthdadjvtx 27513	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
153	151, 152	syl3an3 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
154		df-2 11703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 = (1 + 1)
155	154	fveq2i 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
156	155	neeq2i 3083	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157	153, 156	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
158		ax-1ne0 10608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
159		fzo1fzo0n0 13091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
160	148, 158, 159	mpbir2an 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ (1..^4)
161	160, 121	eleqtrrid 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ∈ (1..^(♯‘𝐹)))
162		3re 11720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ ℝ
163		4re 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 4 ∈ ℝ
164	162, 163, 90	ltleii 10765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ≤ 4
165		elfz2nn0 13001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (3 ∈ (0...4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀ ∧ 3 ≤ 4))
166	88, 54, 164, 165	mpbir3an 1337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ∈ (0...4)
167	166, 58	eleqtrrid 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (0...(♯‘𝐹)))
168		1re 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ∈ ℝ
169		1lt3 11813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 3
170	168, 169	ltneii 10755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ≠ 3
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ≠ 3)
172	161, 167, 171	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐹) = 4 → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
173	172	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
174	173	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
175		pthdivtx 27512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
176	115, 174, 175	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
177		eleq2 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (2 ∈ (0..^(♯‘𝐹)) ↔ 2 ∈ (0..^4)))
178	117, 177	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 2 ∈ (0..^(♯‘𝐹)))
179	178	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 2 ∈ (0..^(♯‘𝐹)))
180		pthdadjvtx 27513	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
181	179, 180	syl3an3 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
182		df-3 11704	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 3 = (2 + 1)
183	182	fveq2i 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
184	183	neeq2i 3083	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185	181, 184	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
186	157, 176, 185	3jca 1124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
187	146, 186	jca 514	. . . . . . . . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
189	188	adantr 483	. . . . . . . . . . . . . . . . . . . . 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 4672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
191	190	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
192	191	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
193		preq1 4671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
194	193	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
195	194	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
196	192, 195	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
197		neeq2 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
198	197	3anbi2d 1437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
199		neeq2 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
200		neeq1 3080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑))
201	199, 200	3anbi13d 1434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
202	198, 201	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
203	196, 202	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 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 4672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
205	204	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
206		preq1 4671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
207	206	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
208	205, 207	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
209	208	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
210		neeq2 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
211	210	3anbi3d 1438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
212		neeq2 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
213		neeq2 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
214	212, 213	3anbi23d 1435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
215	211, 214	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . . . . . . . . . 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 3637	. . . . . . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . . . . . 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 1124	. . . . . . . . . . . . . . . . . . 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 422	. . . . . . . . . . . . . . . . . 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 697	. . . . . . . . . . . . . . . . 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 483	. . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . 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 422	. . . . . . . . . . . . . 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 426	. . . . . . . . . . . . 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 4671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
227	226	eleq1d 2899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
228	227	anbi1d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
229		preq2 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
230	229	eleq1d 2899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
231	230	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
232	228, 231	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
233		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
234		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐))
235		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑))
236	233, 234, 235	3anbi123d 1432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
237	236	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → (((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
238	232, 237	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
239	238	2rexbidv 3302	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
240		preq2 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
241	240	eleq1d 2899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
242		preq1 4671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
243	242	eleq1d 2899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
244	241, 243	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
245	244	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
246		neeq2 3081	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
247	246	3anbi1d 1436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
248		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
249		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑))
250	248, 249	3anbi12d 1433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → ((𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))
251	247, 250	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
252	245, 251	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
253	252	2rexbidv 3302	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
254	239, 253	rspc2ev 3637	. . . . . . . . . . . . 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 242	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
257	256	expd 418	. . . . . . . . . 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 416	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
261	260	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
262	261	expd 418	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
263	2, 262	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
264	263	imp 409	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
265	1, 264	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
266	265	3imp21 1110	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 ∪ cun 3936 {cpr 4571 class class class wbr 5068 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 0cc0 10539 1c1 10540 + caddc 10542 < clt 10677 ≤ cle 10678 ℕcn 11640 2c2 11695 3c3 11696 4c4 11697 ℕ₀cn0 11900 ...cfz 12895 ..^cfzo 13036 ♯chash 13693 Vtxcvtx 26783 Edgcedg 26834 UPGraphcupgr 26867 Walkscwlks 27380 Pathscpths 27495 Cyclesccycls 27568

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ifp 1058 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-pm 8411 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-dju 9332 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-n0 11901 df-xnn0 11971 df-z 11985 df-uz 12247 df-fz 12896 df-fzo 13037 df-hash 13694 df-word 13865 df-edg 26835 df-uhgr 26845 df-upgr 26869 df-wlks 27383 df-trls 27476 df-pths 27499 df-cycls 27570

This theorem is referenced by: n4cyclfrgr 28072

W3C validator