Metamath Proof Explorer

Theorem upgr3v3e3cycl

Description: If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 upgr3v3e3cycl.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 upgr3v3e3cycl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 cyclprop ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
5 1 upgrwlkvtxedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 )
6 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 3 ) )
7 6 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) )
8 7 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ) )
9 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 3 ) )
10 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
11 9 10 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 , 2 } )
12 11 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑘 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
13 c0ex ⊢ 0 ∈ V
14 1ex ⊢ 1 ∈ V
15 2ex ⊢ 2 ∈ 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 fveq2 ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 2 ) )
28 oveq1 ⊢ ( 𝑘 = 2 → ( 𝑘 + 1 ) = ( 2 + 1 ) )
29 2p1e3 ⊢ ( 2 + 1 ) = 3
30 28 29 eqtrdi ⊢ ( 𝑘 = 2 → ( 𝑘 + 1 ) = 3 )
31 30 fveq2d ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 3 ) )
32 27 31 preq12d ⊢ ( 𝑘 = 2 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } )
33 32 eleq1d ⊢ ( 𝑘 = 2 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) )
34 13 14 15 19 26 33 raltp ⊢ ( ∀ 𝑘 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) )
35 12 34 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) )
36 8 35 anbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) ↔ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) ) )
37 2 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
38 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 3 ) )
39 38 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 ) )
40 id ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 )
41 3nn0 ⊢ 3 ∈ ℕ0
42 0elfz ⊢ ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
43 41 42 mp1i ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → 0 ∈ ( 0 ... 3 ) )
44 40 43 ffvelrnd ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
45 1nn0 ⊢ 1 ∈ ℕ0
46 1lt3 ⊢ 1 < 3
47 fvffz0 ⊢ ( ( ( 3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3 ) ∧ 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
48 47 ex ⊢ ( ( 3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3 ) → ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( 𝑃 ‘ 1 ) ∈ 𝑉 ) )
49 41 45 46 48 mp3an ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
50 2nn0 ⊢ 2 ∈ ℕ0
51 2lt3 ⊢ 2 < 3
52 fvffz0 ⊢ ( ( ( 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3 ) ∧ 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
53 52 ex ⊢ ( ( 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3 ) → ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
54 41 50 51 53 mp3an ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
55 44 49 54 3jca ⊢ ( 𝑃 : ( 0 ... 3 ) ⟶ 𝑉 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
56 39 55 syl6bi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
57 56 com12 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
58 4 37 57 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
59 58 adantr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
60 59 adantr ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
61 60 impcom ⊢ ( ( ( ♯ ‘ 𝐹 ) = 3 ∧ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
62 preq2 ⊢ ( ( 𝑃 ‘ 3 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } )
63 62 eqcoms ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } )
64 63 adantl ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } )
65 64 eleq1d ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
66 65 3anbi3d ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
67 66 biimpa ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
68 67 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 3 ∧ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
69 simpll ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
70 breq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 1 < ( ♯ ‘ 𝐹 ) ↔ 1 < 3 ) )
71 46 70 mpbiri ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 1 < ( ♯ ‘ 𝐹 ) )
72 71 adantl ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 1 < ( ♯ ‘ 𝐹 ) )
73 3nn ⊢ 3 ∈ ℕ
74 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
75 73 74 mpbir ⊢ 0 ∈ ( 0 ..^ 3 )
76 75 9 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
77 76 adantl ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
78 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 0 + 1 ) ) )
79 1e0p1 ⊢ 1 = ( 0 + 1 )
80 79 fveq2i ⊢ ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ ( 0 + 1 ) )
81 80 neeq2i ⊢ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( 0 + 1 ) ) )
82 78 81 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
83 69 72 77 82 syl3anc ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
84 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1 < 3 ) )
85 45 73 46 84 mpbir3an ⊢ 1 ∈ ( 0 ..^ 3 )
86 85 9 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
87 86 adantl ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
88 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ ( 1 + 1 ) ) )
89 df-2 ⊢ 2 = ( 1 + 1 )
90 89 fveq2i ⊢ ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( 1 + 1 ) )
91 90 neeq2i ⊢ ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ ( 1 + 1 ) ) )
92 88 91 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) )
93 69 72 87 92 syl3anc ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) )
94 elfzo0 ⊢ ( 2 ∈ ( 0 ..^ 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3 ) )
95 50 73 51 94 mpbir3an ⊢ 2 ∈ ( 0 ..^ 3 )
96 95 9 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
97 96 adantl ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
98 pthdadjvtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 2 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
99 69 72 97 98 syl3anc ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
100 neeq2 ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ) )
101 df-3 ⊢ 3 = ( 2 + 1 )
102 101 fveq2i ⊢ ( 𝑃 ‘ 3 ) = ( 𝑃 ‘ ( 2 + 1 ) )
103 102 neeq2i ⊢ ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 3 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) )
104 100 103 bitrdi ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) ) )
105 104 adantl ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) ) )
106 105 adantr ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ ( 2 + 1 ) ) ) )
107 99 106 mpbird ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) )
108 83 93 107 3jca ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) )
109 108 ex ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) ) )
110 109 adantr ⊢ ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) ) )
111 110 impcom ⊢ ( ( ( ♯ ‘ 𝐹 ) = 3 ∧ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) )
112 preq1 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → { 𝑎 , 𝑏 } = { ( 𝑃 ‘ 0 ) , 𝑏 } )
113 112 eleq1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ) )
114 preq2 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → { 𝑐 , 𝑎 } = { 𝑐 , ( 𝑃 ‘ 0 ) } )
115 114 eleq1d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( { 𝑐 , 𝑎 } ∈ 𝐸 ↔ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
116 113 115 3anbi13d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
117 neeq1 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑃 ‘ 0 ) ≠ 𝑏 ) )
118 neeq2 ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( 𝑐 ≠ 𝑎 ↔ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) )
119 117 118 3anbi13d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) )
120 116 119 anbi12d ⊢ ( 𝑎 = ( 𝑃 ‘ 0 ) → ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) ) )
121 preq2 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → { ( 𝑃 ‘ 0 ) , 𝑏 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
122 121 eleq1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ) )
123 preq1 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → { 𝑏 , 𝑐 } = { ( 𝑃 ‘ 1 ) , 𝑐 } )
124 123 eleq1d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( { 𝑏 , 𝑐 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ) )
125 122 124 3anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
126 neeq2 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
127 neeq1 ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( 𝑏 ≠ 𝑐 ↔ ( 𝑃 ‘ 1 ) ≠ 𝑐 ) )
128 126 127 3anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) )
129 125 128 anbi12d ⊢ ( 𝑏 = ( 𝑃 ‘ 1 ) → ( ( ( { ( 𝑃 ‘ 0 ) , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) ) )
130 preq2 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 1 ) , 𝑐 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
131 130 eleq1d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ) )
132 preq1 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → { 𝑐 , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } )
133 132 eleq1d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) )
134 131 133 3anbi23d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ) )
135 neeq2 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( 𝑃 ‘ 1 ) ≠ 𝑐 ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
136 neeq1 ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( 𝑐 ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) )
137 135 136 3anbi23d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) ) )
138 134 137 anbi12d ⊢ ( 𝑐 = ( 𝑃 ‘ 2 ) → ( ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ 𝑐 ∧ 𝑐 ≠ ( 𝑃 ‘ 0 ) ) ) ↔ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) ) ) )
139 120 129 138 rspc3ev ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ∧ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ 𝐸 ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) )
140 61 68 111 139 syl12anc ⊢ ( ( ( ♯ ‘ 𝐹 ) = 3 ∧ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) )
141 140 ex ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ 𝐸 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) )
142 36 141 sylbid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) )
143 142 expd ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) )
144 143 com13 ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) )
145 5 144 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) )
146 145 expcom ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) ) )
147 146 com23 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) ) )
148 147 expd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) ) ) )
149 4 148 mpcom ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) ) )
150 149 imp ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) )
151 3 150 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 3 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) ) ) )
152 151 3imp21 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ) )