Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
2 | 1 | ewlkprop 27545 |
. . 3
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*)
∧ 𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
3 | | fvex 6687 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V |
4 | | hashin 13864 |
. . . . . . . . . . 11
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) |
6 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → 𝐺 ∈ UPGraph) |
7 | | upgruhgr 27047 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
8 | 1 | uhgrfun 27011 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
10 | 9 | funfnd 6370 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
11 | 10 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
12 | 11 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
13 | | elfzofz 13144 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(1..^(♯‘𝐹))
→ 𝑘 ∈
(1...(♯‘𝐹))) |
14 | | fz1fzo0m1 13176 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(1...(♯‘𝐹))
→ (𝑘 − 1) ∈
(0..^(♯‘𝐹))) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(1..^(♯‘𝐹))
→ (𝑘 − 1) ∈
(0..^(♯‘𝐹))) |
16 | | wrdsymbcl 13968 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ (𝑘 − 1) ∈
(0..^(♯‘𝐹)))
→ (𝐹‘(𝑘 − 1)) ∈ dom
(iEdg‘𝐺)) |
17 | 15, 16 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈
(1..^(♯‘𝐹)))
→ (𝐹‘(𝑘 − 1)) ∈ dom
(iEdg‘𝐺)) |
18 | 17 | 3ad2antl2 1187 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) |
19 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
20 | 19, 1 | upgrle 27035 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) →
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
21 | 6, 12, 18, 20 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
22 | 3 | inex1 5185 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V |
23 | | hashxrcl 13810 |
. . . . . . . . . . . . . . 15
⊢
((((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ* |
25 | | hashxrcl 13810 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ*) |
26 | 3, 25 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ* |
27 | | 2re 11790 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
28 | 27 | rexri 10777 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ* |
29 | 24, 26, 28 | 3pm3.2i 1340 |
. . . . . . . . . . . . 13
⊢
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*) |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) →
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*)) |
31 | | xrletr 12634 |
. . . . . . . . . . . 12
⊢
(((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*) → (((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∧
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) →
(((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∧
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
33 | 21, 32 | mpan2d 694 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) →
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
34 | 5, 33 | mpi 20 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) |
35 | | xnn0xr 12053 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 𝑆 ∈
ℝ*) |
36 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
37 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 2 ∈
ℝ*) |
38 | | xrletr 12634 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧ 2
∈ ℝ*) → ((𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
39 | 35, 36, 37, 38 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
ℕ0* → ((𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
40 | 39 | expcomd 420 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
ℕ0* → ((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
41 | 40 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → ((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) →
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
43 | 42 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) →
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
44 | 34, 43 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2)) |
45 | 44 | ralimdva 3091 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2)) |
46 | 45 | 3exp 1120 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (𝐺 ∈ UPGraph → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2)))) |
47 | 46 | com34 91 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → (𝐺 ∈ UPGraph → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2)))) |
48 | 47 | 3imp 1112 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐺 ∈ UPGraph → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2)) |
49 | | lencl 13974 |
. . . . . 6
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(♯‘𝐹) ∈
ℕ0) |
50 | | 1zzd 12094 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℤ) |
51 | | nn0z 12086 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℤ) |
52 | | fzon 13149 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) →
((♯‘𝐹) ≤ 1
↔ (1..^(♯‘𝐹)) = ∅)) |
53 | 50, 51, 52 | syl2anc 587 |
. . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≤ 1 ↔ (1..^(♯‘𝐹)) = ∅)) |
54 | | nn0re 11985 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℝ) |
55 | | 1red 10720 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℝ) |
56 | 54, 55 | lenltd 10864 |
. . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≤ 1 ↔ ¬ 1 <
(♯‘𝐹))) |
57 | 53, 56 | bitr3d 284 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℕ0 → ((1..^(♯‘𝐹)) = ∅ ↔ ¬ 1 <
(♯‘𝐹))) |
58 | 57 | biimpd 232 |
. . . . . . . . 9
⊢
((♯‘𝐹)
∈ ℕ0 → ((1..^(♯‘𝐹)) = ∅ → ¬ 1 <
(♯‘𝐹))) |
59 | 58 | necon2ad 2949 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ0 → (1 < (♯‘𝐹) → (1..^(♯‘𝐹)) ≠
∅)) |
60 | | rspn0 4241 |
. . . . . . . 8
⊢
((1..^(♯‘𝐹)) ≠ ∅ → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2)) |
61 | 59, 60 | syl6com 37 |
. . . . . . 7
⊢ (1 <
(♯‘𝐹) →
((♯‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2))) |
62 | 61 | com3l 89 |
. . . . . 6
⊢
((♯‘𝐹)
∈ ℕ0 → (∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2 → (1 < (♯‘𝐹) → 𝑆 ≤ 2))) |
63 | 49, 62 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2 → (1 < (♯‘𝐹) → 𝑆 ≤ 2))) |
64 | 63 | 3ad2ant2 1135 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2 → (1 < (♯‘𝐹) → 𝑆 ≤ 2))) |
65 | 48, 64 | syld 47 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐺 ∈ UPGraph → (1 <
(♯‘𝐹) →
𝑆 ≤
2))) |
66 | 2, 65 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → (𝐺 ∈ UPGraph → (1 <
(♯‘𝐹) →
𝑆 ≤
2))) |
67 | 66 | 3imp21 1115 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (♯‘𝐹)) → 𝑆 ≤ 2) |