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 30204

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 29813	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 29745	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		upgr4cycl4dv4e.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
4	3	upgrwlkvtxedg 29663	. . . . . . . . 9 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (𝑃‘(♯‘𝐹)) = (𝑃‘4))
6	5	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
7	6	anbi2d 630	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8		oveq2 7439	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = (0..^4))
9		fzo0to42pr 13792	. . . . . . . . . . . . . . . 16 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
10	8, 9	eqtrdi 2793	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) = 4 → (0..^(♯‘𝐹)) = ({0, 1} ∪ {2, 3}))
11	10	raleqdv 3326	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12		ralunb 4197	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13		c0ex 11255	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
14		1ex 11257	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
15		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0))
16		fv0p1e1 12389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
17	15, 16	preq12d 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
18	17	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
19		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1))
20		oveq1 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
21		1p1e2 12391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
22	20, 21	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 1 → (𝑘 + 1) = 2)
23	22	fveq2d 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
24	19, 23	preq12d 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
25	24	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
26	13, 14, 18, 25	ralpr 4700	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
27		2ex 12343	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ V
28		3ex 12348	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ V
29		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2))
30		oveq1 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31		2p1e3 12408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
32	30, 31	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 2 → (𝑘 + 1) = 3)
33	32	fveq2d 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
34	29, 33	preq12d 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
35	34	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
36		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3))
37		oveq1 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
38		3p1e4 12411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 + 1) = 4
39	37, 38	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 3 → (𝑘 + 1) = 4)
40	39	fveq2d 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
41	36, 40	preq12d 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
42	41	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
43	27, 28, 35, 42	ralpr 4700	. . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
46	11, 45	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
47	7, 46	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
48		preq2 4734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
49	48	eleq1d 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
50	49	eqcoms 2745	. . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
54		4nn0 12545	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ₀)
56		upgr4cycl4dv4e.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 29634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) = 4 → (0...(♯‘𝐹)) = (0...4))
59	58	feq2d 6722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) = 4 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉))
60	59	biimpcd 249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
61	2, 57, 60	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
62	61	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
63		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℕ₀)
64		0nn0 12541	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ₀
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 ∈ ℕ₀)
66		4pos 12373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 < 4
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 0 < 4)
68	63, 65, 67	3jca 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4))
69		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 0 ∈ ℕ₀ ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
70	68, 69	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
71	70	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
72		1nn0 12542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 ∈ ℕ₀)
74		1lt4 12442	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 < 4
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → 1 < 4)
76	63, 73, 75	3jca 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4))
77		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((4 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
78	76, 77	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
80		2nn0 12543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ₀
81	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 ∈ ℕ₀)
82		2lt4 12441	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 2 < 4)
84	63, 81, 83	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4))
85		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
86	84, 85	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
87	86	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
88		3nn0 12544	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ₀
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 ∈ ℕ₀)
90		3lt4 12440	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 < 4
91	90	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℕ₀ → 3 < 4)
92	63, 89, 91	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℕ₀ → (4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4))
93		fvffz0 13686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
94	92, 93	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
95	94	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
96		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
97		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
98		breq2 5147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝐹) = 4 → (1 < (♯‘𝐹) ↔ 1 < 4))
99	74, 98	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝐹) = 4 → 1 < (♯‘𝐹))
100	99	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → 1 < (♯‘𝐹))
101		simpll 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (♯‘𝐹) = 4)
102	8	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (0..^(♯‘𝐹)) = (0..^4))
103		4nn 12349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 4 ∈ ℕ
104		lbfzo0 13739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
105	103, 104	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ (0..^4)
106		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^4)))
107	105, 106	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 0 ∈ (0..^(♯‘𝐹)))
108	107	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 0 ∈ (0..^(♯‘𝐹)))
109		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
110	108, 109	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
111		1e0p1 12775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 = (0 + 1)
112	111	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘1) = (𝑃‘(0 + 1))
113	112	neeq2i 3006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114	110, 113	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
115		simp1 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
116		elfzo0 13740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 ∈ (0..^4) ↔ (2 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 2 < 4))
117	80, 103, 82, 116	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ (0..^4)
118		2ne0 12370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ≠ 0
119		fzo1fzo0n0 13754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
120	117, 118, 119	mpbir2an 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 2 ∈ (1..^4)
121		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝐹) = 4 → (1..^(♯‘𝐹)) = (1..^4))
122	120, 121	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ∈ (1..^(♯‘𝐹)))
123		0elfz 13664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 ∈ ℕ₀ → 0 ∈ (0...4))
124	54, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ∈ (0...4)
125	124, 58	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 0 ∈ (0...(♯‘𝐹)))
126	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 2 ≠ 0)
127	122, 125, 126	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
128	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
129	128	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (2 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 2 ≠ 0))
130		pthdivtx 29747	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
133		elfzo0 13740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
134	88, 103, 90, 133	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ (0..^4)
135		3ne0 12372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ≠ 0
136		fzo1fzo0n0 13754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
137	134, 135, 136	mpbir2an 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ∈ (1..^4)
138	137, 121	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (1..^(♯‘𝐹)))
139	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝐹) = 4 → 3 ≠ 0)
140	138, 125, 139	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
142	141	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (3 ∈ (1..^(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ 3 ≠ 0))
143		pthdivtx 29747	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
146	114, 132, 145	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
147		elfzo0 13740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
148	72, 103, 74, 147	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ (0..^4)
149		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈ (0..^4)))
150	148, 149	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 1 ∈ (0..^(♯‘𝐹)))
151	150	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 1 ∈ (0..^(♯‘𝐹)))
152		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
153	151, 152	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
154		df-2 12329	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 2 = (1 + 1)
155	154	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘2) = (𝑃‘(1 + 1))
156	155	neeq2i 3006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157	153, 156	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
158		ax-1ne0 11224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
159		fzo1fzo0n0 13754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
160	148, 158, 159	mpbir2an 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ (1..^4)
161	160, 121	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ∈ (1..^(♯‘𝐹)))
162		3re 12346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 3 ∈ ℝ
163		4re 12350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 4 ∈ ℝ
164	162, 163, 90	ltleii 11384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 3 ≤ 4
165		elfz2nn0 13658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (3 ∈ (0...4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀ ∧ 3 ≤ 4))
166	88, 54, 164, 165	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ∈ (0...4)
167	166, 58	eleqtrrid 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 3 ∈ (0...(♯‘𝐹)))
168		1re 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ∈ ℝ
169		1lt3 12439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 < 3
170	168, 169	ltneii 11374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ≠ 3
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝐹) = 4 → 1 ≠ 3)
172	161, 167, 171	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝐹) = 4 → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
173	172	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
174	173	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (1 ∈ (1..^(♯‘𝐹)) ∧ 3 ∈ (0...(♯‘𝐹)) ∧ 1 ≠ 3))
175		pthdivtx 29747	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → (2 ∈ (0..^(♯‘𝐹)) ↔ 2 ∈ (0..^4)))
178	117, 177	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0..^(♯‘𝐹)) = (0..^4) → 2 ∈ (0..^(♯‘𝐹)))
179	178	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4)) → 2 ∈ (0..^(♯‘𝐹)))
180		pthdadjvtx 29748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
181	179, 180	syl3an3 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
182		df-3 12330	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 3 = (2 + 1)
183	182	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃‘3) = (𝑃‘(2 + 1))
184	183	neeq2i 3006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185	181, 184	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
186	157, 176, 185	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
187	146, 186	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ ((♯‘𝐹) = 4 ∧ (0..^(♯‘𝐹)) = (0..^4))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
188	97, 100, 101, 102, 187	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
190		preq2 4734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
191	190	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
192	191	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
193		preq1 4733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
194	193	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . 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 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
198	197	3anbi2d 1443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
199		neeq2 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
200		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑))
201	199, 200	3anbi13d 1440	. . . . . . . . . . . . . . . . . . . . . . . 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 4734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
205	204	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
206		preq1 4733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
207	206	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . 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 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
211	210	3anbi3d 1444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
212		neeq2 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
213		neeq2 3004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
214	212, 213	3anbi23d 1441	. . . . . . . . . . . . . . . . . . . . . . . 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 3635	. . . . . . . . . . . . . . . . . . . . 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 1376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
219	71, 79, 218	3jca 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
220	219	exp31 419	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → ((4 ∈ ℕ₀ ∧ 𝑃:(0...4)⟶𝑉) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
221	55, 62, 220	mp2and 699	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
222	221	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
223	53, 222	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
224	223	exp31 419	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 4 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
225	224	imp4c 423	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
226		preq1 4733	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
227	226	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
228	227	anbi1d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
229		preq2 4734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
230	229	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
231	230	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
232	228, 231	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
233		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏))
234		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐))
235		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑))
236	233, 234, 235	3anbi123d 1438	. . . . . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
240		preq2 4734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
241	240	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
242		preq1 4733	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
243	242	eleq1d 2826	. . . . . . . . . . . . . . . . . 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 3004	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
247	246	3anbi1d 1442	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
248		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐))
249		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑))
250	248, 249	3anbi12d 1439	. . . . . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
254	239, 253	rspc2ev 3635	. . . . . . . . . . . . 13 ⊢ (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
255	225, 254	syl6 35	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
256	47, 255	sylbid 240	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))
257	256	expd 415	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
258	257	com13 88	. . . . . . . . 9 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
259	4, 258	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
260	259	expcom 413	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
261	260	com23 86	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
262	261	expd 415	. . . . 5 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))))
263	2, 262	mpcom 38	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))
264	263	imp 406	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
265	1, 264	syl 17	. 2 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))
266	265	3imp21 1114	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))

Colors of variables: wff setvar class

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

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

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

This theorem is referenced by: n4cyclfrgr 30310

W3C validator