This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgr4cycl4dv4e

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)

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

Proof

Step Hyp Ref Expression
1 upgr4cycl4dv4e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgr4cycl4dv4e.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 cyclprop ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
5 2 upgrwlkvtxedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 )
6 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 4 ) )
7 6 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) ) )
8 7 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) ) ) )
9 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) )
10 fzo0to42pr ⊢ ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } )
11 9 10 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( { 0 , 1 } ∪ { 2 , 3 } ) )
12 11 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
13 ralunb ⊢ ( ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( ∀ 𝑘 ∈ { 0 , 1 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ∧ ∀ 𝑘 ∈ { 2 , 3 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
14 c0ex ⊢ 0 ∈ V
15 1ex ⊢ 1 ∈ V
16 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
17 fv0p1e1 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
18 16 17 preq12d ⊢ ( 𝑘 = 0 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
19 18 eleq1d ⊢ ( 𝑘 = 0 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ) )
20 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
21 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
22 1p1e2 ⊢ ( 1 + 1 ) = 2
23 21 22 eqtrdi ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = 2 )
24 23 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 2 ) )
25 20 24 preq12d ⊢ ( 𝑘 = 1 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
26 25 eleq1d ⊢ ( 𝑘 = 1 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) )
27 14 15 19 26 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) )
28 2ex ⊢ 2 ∈ V
29 3ex ⊢ 3 ∈ V
30 fveq2 ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 2 ) )
31 oveq1 ⊢ ( 𝑘 = 2 → ( 𝑘 + 1 ) = ( 2 + 1 ) )
32 2p1e3 ⊢ ( 2 + 1 ) = 3
33 31 32 eqtrdi ⊢ ( 𝑘 = 2 → ( 𝑘 + 1 ) = 3 )
34 33 fveq2d ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 3 ) )
35 30 34 preq12d ⊢ ( 𝑘 = 2 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } )
36 35 eleq1d ⊢ ( 𝑘 = 2 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) )
37 fveq2 ⊢ ( 𝑘 = 3 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 3 ) )
38 oveq1 ⊢ ( 𝑘 = 3 → ( 𝑘 + 1 ) = ( 3 + 1 ) )
39 3p1e4 ⊢ ( 3 + 1 ) = 4
40 38 39 eqtrdi ⊢ ( 𝑘 = 3 → ( 𝑘 + 1 ) = 4 )
41 40 fveq2d ⊢ ( 𝑘 = 3 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 4 ) )
42 37 41 preq12d ⊢ ( 𝑘 = 3 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } )
43 42 eleq1d ⊢ ( 𝑘 = 3 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) )
44 28 29 36 43 ralpr ⊢ ( ∀ 𝑘 ∈ { 2 , 3 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) )
45 27 44 anbi12i ⊢ ( ( ∀ 𝑘 ∈ { 0 , 1 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ∧ ∀ 𝑘 ∈ { 2 , 3 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) )
46 13 45 bitri ⊢ ( ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) )
47 12 46 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) ) )
48 8 47 anbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) ↔ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) ) ) )
49 preq2 ⊢ ( ( 𝑃 ‘ 4 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } = { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } )
50 49 eleq1d ⊢ ( ( 𝑃 ‘ 4 ) = ( 𝑃 ‘ 0 ) → ( { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
51 50 eqcoms ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) → ( { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
52 51 anbi2d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) → ( ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
53 52 anbi2d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
54 53 adantl ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
55 4nn0 ⊢ 4 ∈ ℕ0
56 55 a1i ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → 4 ∈ ℕ0 )
57 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
58 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 4 ) )
59 58 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) )
60 59 biimpcd ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝐹 ) = 4 → 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) )
61 4 57 60 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 4 → 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) )
62 61 impcom ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 )
63 id ⊢ ( 4 ∈ ℕ0 → 4 ∈ ℕ0 )
64 0nn0 ⊢ 0 ∈ ℕ0
65 64 a1i ⊢ ( 4 ∈ ℕ0 → 0 ∈ ℕ0 )
66 4pos ⊢ 0 < 4
67 66 a1i ⊢ ( 4 ∈ ℕ0 → 0 < 4 )
68 63 65 67 3jca ⊢ ( 4 ∈ ℕ0 → ( 4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4 ) )
69 fvffz0 ⊢ ( ( ( 4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4 ) ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
70 68 69 sylan ⊢ ( ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
71 70 ad2antlr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
72 1nn0 ⊢ 1 ∈ ℕ0
73 72 a1i ⊢ ( 4 ∈ ℕ0 → 1 ∈ ℕ0 )
74 1lt4 ⊢ 1 < 4
75 74 a1i ⊢ ( 4 ∈ ℕ0 → 1 < 4 )
76 63 73 75 3jca ⊢ ( 4 ∈ ℕ0 → ( 4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4 ) )
77 fvffz0 ⊢ ( ( ( 4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4 ) ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
78 76 77 sylan ⊢ ( ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
79 78 ad2antlr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
80 2nn0 ⊢ 2 ∈ ℕ0
81 80 a1i ⊢ ( 4 ∈ ℕ0 → 2 ∈ ℕ0 )
82 2lt4 ⊢ 2 < 4
83 82 a1i ⊢ ( 4 ∈ ℕ0 → 2 < 4 )
84 63 81 83 3jca ⊢ ( 4 ∈ ℕ0 → ( 4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4 ) )
85 fvffz0 ⊢ ( ( ( 4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4 ) ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
86 84 85 sylan ⊢ ( ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
87 86 ad2antlr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
88 3nn0 ⊢ 3 ∈ ℕ0
89 88 a1i ⊢ ( 4 ∈ ℕ0 → 3 ∈ ℕ0 )
90 3lt4 ⊢ 3 < 4
91 90 a1i ⊢ ( 4 ∈ ℕ0 → 3 < 4 )
92 63 89 91 3jca ⊢ ( 4 ∈ ℕ0 → ( 4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4 ) )
93 fvffz0 ⊢ ( ( ( 4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4 ) ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 3 ) ∈ 𝑉 )
94 92 93 sylan ⊢ ( ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 3 ) ∈ 𝑉 )
95 94 ad2antlr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( 𝑃 ‘ 3 ) ∈ 𝑉 )
96 simpr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
97 simplr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
98 breq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 1 < ( ♯ ‘ 𝐹 ) ↔ 1 < 4 ) )
99 74 98 mpbiri ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 1 < ( ♯ ‘ 𝐹 ) )
100 99 ad2antrr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) → 1 < ( ♯ ‘ 𝐹 ) )
101 simpll ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) → ( ♯ ‘ 𝐹 ) = 4 )
102 9 ad2antrr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) )
103 4nn ⊢ 4 ∈ ℕ
104 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 4 ) ↔ 4 ∈ ℕ )
105 103 104 mpbir ⊢ 0 ∈ ( 0 ..^ 4 )
106 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 0 ∈ ( 0 ..^ 4 ) ) )
107 105 106 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
108 107 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
109 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 0 + 1 ) ) )
110 108 109 syl3an3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 0 + 1 ) ) )
111 1e0p1 ⊢ 1 = ( 0 + 1 )
112 111 fveq2i ⊢ ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ ( 0 + 1 ) )
113 112 neeq2i ⊢ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 0 + 1 ) ) )
114 110 113 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
115 simp1 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
116 elfzo0 ⊢ ( 2 ∈ ( 0 ..^ 4 ) ↔ ( 2 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 2 < 4 ) )
117 80 103 82 116 mpbir3an ⊢ 2 ∈ ( 0 ..^ 4 )
118 2ne0 ⊢ 2 ≠ 0
119 fzo1fzo0n0 ⊢ ( 2 ∈ ( 1 ..^ 4 ) ↔ ( 2 ∈ ( 0 ..^ 4 ) ∧ 2 ≠ 0 ) )
120 117 118 119 mpbir2an ⊢ 2 ∈ ( 1 ..^ 4 )
121 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 4 ) )
122 120 121 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 2 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
123 0elfz ⊢ ( 4 ∈ ℕ0 → 0 ∈ ( 0 ... 4 ) )
124 55 123 ax-mp ⊢ 0 ∈ ( 0 ... 4 )
125 124 58 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
126 118 a1i ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 2 ≠ 0 )
127 122 125 126 3jca ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 2 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 2 ≠ 0 ) )
128 127 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → ( 2 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 2 ≠ 0 ) )
129 128 3ad2ant3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 2 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 2 ≠ 0 ) )
130 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 2 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 2 ≠ 0 ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) )
131 115 129 130 syl2anc ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) )
132 131 necomd ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) )
133 elfzo0 ⊢ ( 3 ∈ ( 0 ..^ 4 ) ↔ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 3 < 4 ) )
134 88 103 90 133 mpbir3an ⊢ 3 ∈ ( 0 ..^ 4 )
135 3ne0 ⊢ 3 ≠ 0
136 fzo1fzo0n0 ⊢ ( 3 ∈ ( 1 ..^ 4 ) ↔ ( 3 ∈ ( 0 ..^ 4 ) ∧ 3 ≠ 0 ) )
137 134 135 136 mpbir2an ⊢ 3 ∈ ( 1 ..^ 4 )
138 137 121 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 3 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
139 135 a1i ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 3 ≠ 0 )
140 138 125 139 3jca ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 3 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 3 ≠ 0 ) )
141 140 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → ( 3 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 3 ≠ 0 ) )
142 141 3ad2ant3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 3 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 3 ≠ 0 ) )
143 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 3 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 3 ≠ 0 ) ) → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 0 ) )
144 115 142 143 syl2anc ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 3 ) ≠ ( 𝑃 ‘ 0 ) )
145 144 necomd ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) )
146 114 132 145 3jca ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) ) )
147 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 4 ) ↔ ( 1 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 1 < 4 ) )
148 72 103 74 147 mpbir3an ⊢ 1 ∈ ( 0 ..^ 4 )
149 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 1 ∈ ( 0 ..^ 4 ) ) )
150 148 149 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
151 150 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
152 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ ( 1 + 1 ) ) )
153 151 152 syl3an3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ ( 1 + 1 ) ) )
154 df-2 ⊢ 2 = ( 1 + 1 )
155 154 fveq2i ⊢ ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( 1 + 1 ) )
156 155 neeq2i ⊢ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ ( 1 + 1 ) ) )
157 153 156 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) )
158 ax-1ne0 ⊢ 1 ≠ 0
159 fzo1fzo0n0 ⊢ ( 1 ∈ ( 1 ..^ 4 ) ↔ ( 1 ∈ ( 0 ..^ 4 ) ∧ 1 ≠ 0 ) )
160 148 158 159 mpbir2an ⊢ 1 ∈ ( 1 ..^ 4 )
161 160 121 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
162 3re ⊢ 3 ∈ ℝ
163 4re ⊢ 4 ∈ ℝ
164 162 163 90 ltleii ⊢ 3 ≤ 4
165 elfz2nn0 ⊢ ( 3 ∈ ( 0 ... 4 ) ↔ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4 ) )
166 88 55 164 165 mpbir3an ⊢ 3 ∈ ( 0 ... 4 )
167 166 58 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
168 1re ⊢ 1 ∈ ℝ
169 1lt3 ⊢ 1 < 3
170 168 169 ltneii ⊢ 1 ≠ 3
171 170 a1i ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → 1 ≠ 3 )
172 161 167 171 3jca ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 3 ) )
173 172 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 3 ) )
174 173 3ad2ant3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 3 ) )
175 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 3 ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) )
176 115 174 175 syl2anc ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) )
177 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → ( 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 2 ∈ ( 0 ..^ 4 ) ) )
178 117 177 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
179 178 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
180 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
181 179 180 syl3an3 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
182 df-3 ⊢ 3 = ( 2 + 1 )
183 182 fveq2i ⊢ ( 𝑃 ‘ 3 ) = ( 𝑃 ‘ ( 2 + 1 ) )
184 183 neeq2i ⊢ ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
185 181 184 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) )
186 157 176 185 3jca ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ ( ( ♯ ‘ 𝐹 ) = 4 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 4 ) ) ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) )
187 146 186 jca ⊢ ( ( 𝐹 ( 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 ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) ) ∧ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) ) )
189 188 adantr ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) ) ∧ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) ) )
190 preq2 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 1 ) , 𝑐 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
191 190 eleq1d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) )
192 191 anbi2d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ) )
193 preq1 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → { 𝑐 , 𝑑 } = { ( 𝑃 ‘ 2 ) , 𝑑 } )
194 193 eleq1d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ) )
195 194 anbi1d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
196 192 195 anbi12d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
197 neeq2 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( 𝑃 ‘ 0 ) ≠ 𝑐 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
198 197 3anbi2d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ) )
199 neeq2 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
200 neeq1 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( 𝑐 ≠ 𝑑 ↔ ( 𝑃 ‘ 2 ) ≠ 𝑑 ) )
201 199 200 3anbi13d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ ( 𝑃 ‘ 2 ) ≠ 𝑑 ) ) )
202 198 201 anbi12d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ ( 𝑃 ‘ 2 ) ≠ 𝑑 ) ) ) )
203 196 202 anbi12d ⊢ ( 𝑐 = ( 𝑃 ‘ 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 ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 2 ) , 𝑑 } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } )
205 204 eleq1d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) )
206 preq1 ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → { 𝑑 , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } )
207 206 eleq1d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
208 205 207 anbi12d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
209 208 anbi2d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
210 neeq2 ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( 𝑃 ‘ 0 ) ≠ 𝑑 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) ) )
211 210 3anbi3d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 3 ) ) ) )
212 neeq2 ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( 𝑃 ‘ 1 ) ≠ 𝑑 ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ) )
213 neeq2 ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( 𝑃 ‘ 2 ) ≠ 𝑑 ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) )
214 212 213 3anbi23d ⊢ ( 𝑑 = ( 𝑃 ‘ 3 ) → ( ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ ( 𝑃 ‘ 2 ) ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 3 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) ) )
215 211 214 anbi12d ⊢ ( 𝑑 = ( 𝑃 ‘ 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 ⊢ ( 𝑑 = ( 𝑃 ‘ 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 ⊢ ( ( ( 𝑃 ‘ 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 ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 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 ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( 4 ∈ ℕ0 ∧ 𝑃 : ( 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 ⊢ ( ( ( ♯ ‘ 𝐹 ) = 4 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( 4 ∈ ℕ0 ∧ 𝑃 : ( 0 ... 4 ) ⟶ 𝑉 ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) ) )
221 56 62 220 mp2and ⊢ ( ( ( ♯ ‘ 𝐹 ) = 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 ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 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 54 222 sylbid ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 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 ⊢ ( ( ♯ ‘ 𝐹 ) = 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 ⊢ ( ( ♯ ‘ 𝐹 ) = 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 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → { 𝑎 , 𝑏 } = { ( 𝑃 ‘ 0 ) , 𝑏 } )
227 226 eleq1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ) )
228 227 anbi1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
229 preq2 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → { 𝑑 , 𝑎 } = { 𝑑 , ( 𝑃 ‘ 0 ) } )
230 229 eleq1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( { 𝑑 , 𝑎 } ∈ 𝐸 ↔ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
231 230 anbi2d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ↔ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
232 228 231 anbi12d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
233 neeq1 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑃 ‘ 0 ) ≠ 𝑏 ) )
234 neeq1 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( 𝑎 ≠ 𝑐 ↔ ( 𝑃 ‘ 0 ) ≠ 𝑐 ) )
235 neeq1 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( 𝑎 ≠ 𝑑 ↔ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) )
236 233 234 235 3anbi123d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ) )
237 236 anbi1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
238 232 237 anbi12d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ↔ ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
239 238 2rexbidv ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ↔ ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
240 preq2 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → { ( 𝑃 ‘ 0 ) , 𝑏 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
241 240 eleq1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ) )
242 preq1 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → { 𝑏 , 𝑐 } = { ( 𝑃 ‘ 1 ) , 𝑐 } )
243 242 eleq1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( { 𝑏 , 𝑐 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) )
244 241 243 anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ) )
245 244 anbi1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ) )
246 neeq2 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
247 246 3anbi1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ) )
248 neeq1 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( 𝑏 ≠ 𝑐 ↔ ( 𝑃 ‘ 1 ) ≠ 𝑐 ) )
249 neeq1 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( 𝑏 ≠ 𝑑 ↔ ( 𝑃 ‘ 1 ) ≠ 𝑑 ) )
250 248 249 3anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ↔ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) )
251 247 250 anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
252 245 251 anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ↔ ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
253 252 2rexbidv ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ↔ ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
254 239 253 rspc2ev ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) ∧ ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 0 ) ≠ 𝑑 ) ∧ ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ ( 𝑃 ‘ 1 ) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
255 225 254 syl6 ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 ) ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) ∧ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 3 ) , ( 𝑃 ‘ 4 ) } ∈ 𝐸 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
256 48 255 sylbid ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) )
257 256 expd ⊢ ( ( ♯ ‘ 𝐹 ) = 4 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) )
258 257 com13 ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) )
259 5 258 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) )
260 259 expcom ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) ) )
261 260 com23 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) ) )
262 261 expd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) ) ) )
263 4 262 mpcom ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) ) )
264 263 imp ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) )
265 3 264 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) ) )
266 265 3imp21 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )