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 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ { 𝑑 , 𝑎 } ∈ 𝐸 ) ) ∧ ( ( 𝑎𝑏𝑎𝑐𝑎𝑑 ) ∧ ( 𝑏𝑐𝑏𝑑𝑐𝑑 ) ) ) )