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

Metamath Proof Explorer

Theorem upgrewlkle2

Description: In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion upgrewlkle2 ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 𝑆 ≤ 2 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2 1 ewlkprop ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
3 fvex ⊢ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∈ V
4 hashin ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∈ V → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) )
5 3 4 ax-mp ⊢ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
6 simpl3 ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ UPGraph )
7 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
8 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
9 7 8 syl ⊢ ( 𝐺 ∈ UPGraph → Fun ( iEdg ‘ 𝐺 ) )
10 9 funfnd ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
11 10 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
12 11 adantr ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
13 elfzofz ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) )
14 fz1fzo0m1 ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
15 13 14 syl ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 wrdsymbcl ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑘 − 1 ) ) ∈ dom ( iEdg ‘ 𝐺 ) )
17 15 16 sylan2 ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑘 − 1 ) ) ∈ dom ( iEdg ‘ 𝐺 ) )
18 17 3ad2antl2 ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑘 − 1 ) ) ∈ dom ( iEdg ‘ 𝐺 ) )
19 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
20 19 1 upgrle ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ≤ 2 )
21 6 12 18 20 syl3anc ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ≤ 2 )
22 3 inex1 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V
23 hashxrcl ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* )
24 22 23 ax-mp ⊢ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ*
25 hashxrcl ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∈ V → ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ℝ* )
26 3 25 ax-mp ⊢ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ℝ*
27 2re ⊢ 2 ∈ ℝ
28 27 rexri ⊢ 2 ∈ ℝ*
29 24 26 28 3pm3.2i ⊢ ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* ∧ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* )
30 29 a1i ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* ∧ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* ) )
31 xrletr ⊢ ( ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* ∧ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* ) → ( ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∧ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ≤ 2 ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 ) )
32 30 31 syl ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ∧ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ≤ 2 ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 ) )
33 21 32 mpan2d ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ ( ♯ ‘ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 ) )
34 5 33 mpi ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 )
35 xnn0xr ⊢ ( 𝑆 ∈ ℕ0* → 𝑆 ∈ ℝ* )
36 24 a1i ⊢ ( 𝑆 ∈ ℕ0* → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* )
37 28 a1i ⊢ ( 𝑆 ∈ ℕ0* → 2 ∈ ℝ* )
38 xrletr ⊢ ( ( 𝑆 ∈ ℝ* ∧ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* ) → ( ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∧ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 ) → 𝑆 ≤ 2 ) )
39 35 36 37 38 syl3anc ⊢ ( 𝑆 ∈ ℕ0* → ( ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∧ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 ) → 𝑆 ≤ 2 ) )
40 39 expcomd ⊢ ( 𝑆 ∈ ℕ0* → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑆 ≤ 2 ) ) )
41 40 adantl ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑆 ≤ 2 ) ) )
42 41 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑆 ≤ 2 ) ) )
43 42 adantr ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ≤ 2 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑆 ≤ 2 ) ) )
44 34 43 mpd ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑆 ≤ 2 ) )
45 44 ralimdva ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 ) )
46 45 3exp ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 ) ) ) )
47 46 com34 ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( 𝐺 ∈ UPGraph → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 ) ) ) )
48 47 3imp ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( 𝐺 ∈ UPGraph → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 ) )
49 lencl ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
50 1zzd ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 1 ∈ ℤ )
51 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
52 fzon ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐹 ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅ ) )
53 50 51 52 syl2anc ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅ ) )
54 nn0re ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℝ )
55 1red ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 1 ∈ ℝ )
56 54 55 lenltd ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝐹 ) ) )
57 53 56 bitr3d ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅ ↔ ¬ 1 < ( ♯ ‘ 𝐹 ) ) )
58 57 biimpd ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅ → ¬ 1 < ( ♯ ‘ 𝐹 ) ) )
59 58 necon2ad ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝐹 ) → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ≠ ∅ ) )
60 rspn0 ⊢ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ≠ ∅ → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 → 𝑆 ≤ 2 ) )
61 59 60 syl6com ⊢ ( 1 < ( ♯ ‘ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 → 𝑆 ≤ 2 ) ) )
62 61 com3l ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 → ( 1 < ( ♯ ‘ 𝐹 ) → 𝑆 ≤ 2 ) ) )
63 49 62 syl ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 → ( 1 < ( ♯ ‘ 𝐹 ) → 𝑆 ≤ 2 ) ) )
64 63 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ 2 → ( 1 < ( ♯ ‘ 𝐹 ) → 𝑆 ≤ 2 ) ) )
65 48 64 syld ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( 𝐺 ∈ UPGraph → ( 1 < ( ♯ ‘ 𝐹 ) → 𝑆 ≤ 2 ) ) )
66 2 65 syl ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( 𝐺 ∈ UPGraph → ( 1 < ( ♯ ‘ 𝐹 ) → 𝑆 ≤ 2 ) ) )
67 66 3imp21 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 𝑆 ≤ 2 )