Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
2 | 1 | ewlkprop 26499 |
. . 3
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*)
∧ 𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(#‘𝐹))𝑆 ≤
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
3 | | fvex 6201 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V |
4 | | hashin 13199 |
. . . . . . . . . . 11
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) |
6 | | simpl3 1066 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → 𝐺 ∈ UPGraph ) |
7 | | upgruhgr 25997 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph
) |
8 | 1 | uhgrfun 25961 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
10 | | funfn 5918 |
. . . . . . . . . . . . . . 15
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
11 | 9, 10 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
12 | 11 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
13 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
14 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
15 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1..^(#‘𝐹)) → 𝑘 ∈ (1...(#‘𝐹))) |
16 | | fz1fzo0m1 12515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...(#‘𝐹)) → (𝑘 − 1) ∈ (0..^(#‘𝐹))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1..^(#‘𝐹)) → (𝑘 − 1) ∈ (0..^(#‘𝐹))) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (𝑘 − 1) ∈ (0..^(#‘𝐹))) |
19 | 14, 18 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ (𝑘 − 1) ∈ (0..^(#‘𝐹)))) |
20 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ (𝑘 − 1) ∈
(0..^(#‘𝐹))) →
(𝐹‘(𝑘 − 1)) ∈ dom
(iEdg‘𝐺)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) |
22 | 21 | 3ad2antl2 1224 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) |
23 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
24 | 23, 1 | upgrle 25985 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) →
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
25 | 6, 13, 22, 24 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
26 | 3 | inex1 4799 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V |
27 | | hashxrcl 13148 |
. . . . . . . . . . . . . . 15
⊢
((((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V →
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ* |
29 | | hashxrcl 13148 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ*) |
30 | 3, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ* |
31 | | 2re 11090 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
32 | 31 | rexri 10097 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ* |
33 | 28, 30, 32 | 3pm3.2i 1239 |
. . . . . . . . . . . . 13
⊢
((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → ((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*)) |
35 | | xrletr 11989 |
. . . . . . . . . . . 12
⊢
(((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈ ℝ*
∧ 2 ∈ ℝ*) → (((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∧
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) →
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∧
(#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) →
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
37 | 25, 36 | mpan2d 710 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → ((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (#‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) →
(#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2)) |
38 | 5, 37 | mpi 20 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) |
39 | | xnn0xr 11368 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 𝑆 ∈
ℝ*) |
40 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
41 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 2 ∈
ℝ*) |
42 | | xrletr 11989 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧ 2
∈ ℝ*) → ((𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
43 | 39, 40, 41, 42 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
ℕ0* → ((𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
44 | 43 | expcomd 454 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
ℕ0* → ((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
45 | 44 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → ((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
46 | 45 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) →
((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
47 | 46 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → ((#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
48 | 38, 47 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ (1..^(#‘𝐹))) → (𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2)) |
49 | 48 | ralimdva 2962 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2)) |
50 | 49 | 3exp 1264 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (𝐺 ∈ UPGraph → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2)))) |
51 | 50 | com34 91 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → (𝐺 ∈ UPGraph → ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2)))) |
52 | 51 | 3imp 1256 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐺 ∈ UPGraph → ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2)) |
53 | | lencl 13324 |
. . . . . 6
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(#‘𝐹) ∈
ℕ0) |
54 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℕ0 → 1 ∈ ℤ) |
55 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℤ) |
56 | 54, 55 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → (1 ∈ ℤ ∧ (#‘𝐹) ∈ ℤ)) |
57 | | fzon 12489 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ (#‘𝐹) ∈ ℤ) → ((#‘𝐹) ≤ 1 ↔
(1..^(#‘𝐹)) =
∅)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ≤ 1 ↔ (1..^(#‘𝐹)) = ∅)) |
59 | 58 | bicomd 213 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) ∈
ℕ0 → ((1..^(#‘𝐹)) = ∅ ↔ (#‘𝐹) ≤ 1)) |
60 | | nn0re 11301 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℝ) |
61 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → 1 ∈ ℝ) |
62 | 60, 61 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ∈ ℝ ∧ 1 ∈
ℝ)) |
63 | | lenlt 10116 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℝ ∧ 1 ∈ ℝ) → ((#‘𝐹) ≤ 1 ↔ ¬ 1 < (#‘𝐹))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ≤ 1 ↔ ¬ 1 < (#‘𝐹))) |
65 | 59, 64 | bitrd 268 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) ∈
ℕ0 → ((1..^(#‘𝐹)) = ∅ ↔ ¬ 1 <
(#‘𝐹))) |
66 | 65 | biimpd 219 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → ((1..^(#‘𝐹)) = ∅ → ¬ 1 <
(#‘𝐹))) |
67 | 66 | necon2ad 2809 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → (1 < (#‘𝐹) → (1..^(#‘𝐹)) ≠ ∅)) |
68 | 67 | impcom 446 |
. . . . . . . . . . 11
⊢ ((1 <
(#‘𝐹) ∧
(#‘𝐹) ∈
ℕ0) → (1..^(#‘𝐹)) ≠ ∅) |
69 | | rspn0 3934 |
. . . . . . . . . . 11
⊢
((1..^(#‘𝐹))
≠ ∅ → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((1 <
(#‘𝐹) ∧
(#‘𝐹) ∈
ℕ0) → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2)) |
71 | 70 | ex 450 |
. . . . . . . . 9
⊢ (1 <
(#‘𝐹) →
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2))) |
72 | 71 | com23 86 |
. . . . . . . 8
⊢ (1 <
(#‘𝐹) →
(∀𝑘 ∈
(1..^(#‘𝐹))𝑆 ≤ 2 → ((#‘𝐹) ∈ ℕ0
→ 𝑆 ≤
2))) |
73 | 72 | com13 88 |
. . . . . . 7
⊢
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → (1 < (#‘𝐹) → 𝑆 ≤ 2))) |
74 | 73 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
((#‘𝐹) ∈
ℕ0 → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → (1 < (#‘𝐹) → 𝑆 ≤ 2)))) |
75 | 53, 74 | mpd 15 |
. . . . 5
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(∀𝑘 ∈
(1..^(#‘𝐹))𝑆 ≤ 2 → (1 <
(#‘𝐹) → 𝑆 ≤ 2))) |
76 | 75 | 3ad2ant2 1083 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ 2 → (1 < (#‘𝐹) → 𝑆 ≤ 2))) |
77 | 52, 76 | syld 47 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐺 ∈ UPGraph → (1 <
(#‘𝐹) → 𝑆 ≤ 2))) |
78 | 2, 77 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → (𝐺 ∈ UPGraph → (1 <
(#‘𝐹) → 𝑆 ≤ 2))) |
79 | 78 | 3imp21 1277 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (#‘𝐹)) → 𝑆 ≤ 2) |