Step | Hyp | Ref
| Expression |
1 | | eqid 2771 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
2 | 1 | ewlkprop 26734 |
. . 3
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*)
∧ 𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
3 | | fvex 6344 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V |
4 | | hashin 13401 |
. . . . . . . . . . 11
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) |
6 | | simpl3 1231 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → 𝐺 ∈ UPGraph) |
7 | | upgruhgr 26218 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
8 | 1 | uhgrfun 26182 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
10 | | funfn 6060 |
. . . . . . . . . . . . . . 15
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
11 | 9, 10 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
12 | 11 | 3ad2ant3 1129 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
13 | 12 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
14 | | simpl 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈
(1..^(♯‘𝐹)))
→ 𝐹 ∈ Word dom
(iEdg‘𝐺)) |
15 | | elfzofz 12693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(1..^(♯‘𝐹))
→ 𝑘 ∈
(1...(♯‘𝐹))) |
16 | | fz1fzo0m1 12724 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(1...(♯‘𝐹))
→ (𝑘 − 1) ∈
(0..^(♯‘𝐹))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(1..^(♯‘𝐹))
→ (𝑘 − 1) ∈
(0..^(♯‘𝐹))) |
18 | 17 | adantl 467 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈
(1..^(♯‘𝐹)))
→ (𝑘 − 1) ∈
(0..^(♯‘𝐹))) |
19 | 14, 18 | jca 501 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈
(1..^(♯‘𝐹)))
→ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ (𝑘 − 1) ∈
(0..^(♯‘𝐹)))) |
20 | | wrdsymbcl 13514 |
. . . . . . . . . . . . . 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 1201 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) |
23 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
24 | 23, 1 | upgrle 26206 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ (𝐹‘(𝑘 − 1)) ∈ dom (iEdg‘𝐺)) →
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
25 | 6, 13, 22, 24 | syl3anc 1476 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) ∧ 𝑘 ∈ (1..^(♯‘𝐹))) → (♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ≤ 2) |
26 | 3 | inex1 4934 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V |
27 | | hashxrcl 13350 |
. . . . . . . . . . . . . . 15
⊢
((((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ* |
29 | | hashxrcl 13350 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V →
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ*) |
30 | 3, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(♯‘((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1)))) ∈
ℝ* |
31 | | 2re 11296 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
32 | 31 | rexri 10303 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ* |
33 | 28, 30, 32 | 3pm3.2i 1423 |
. . . . . . . . . . . . 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 12194 |
. . . . . . . . . . . 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 674 |
. . . . . . . . . 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 11575 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 𝑆 ∈
ℝ*) |
40 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
41 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
ℕ0* → 2 ∈
ℝ*) |
42 | | xrletr 12194 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ* ∧ 2
∈ ℝ*) → ((𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
43 | 39, 40, 41, 42 | syl3anc 1476 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
ℕ0* → ((𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2) → 𝑆 ≤ 2)) |
44 | 43 | expcomd 402 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
ℕ0* → ((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
45 | 44 | adantl 467 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → ((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
46 | 45 | 3ad2ant1 1127 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) →
((♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ≤ 2 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑆 ≤ 2))) |
47 | 46 | adantr 466 |
. . . . . . . . 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 3111 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2)) |
50 | 49 | 3exp 1112 |
. . . . . 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 1101 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐺 ∈ UPGraph → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2)) |
53 | | lencl 13520 |
. . . . . 6
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(♯‘𝐹) ∈
ℕ0) |
54 | | 1zzd 11615 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℤ) |
55 | | nn0z 11607 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℤ) |
56 | 54, 55 | jca 501 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐹)
∈ ℕ0 → (1 ∈ ℤ ∧ (♯‘𝐹) ∈
ℤ)) |
57 | | fzon 12697 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) →
((♯‘𝐹) ≤ 1
↔ (1..^(♯‘𝐹)) = ∅)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ≤ 1 ↔ (1..^(♯‘𝐹)) = ∅)) |
59 | 58 | bicomd 213 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹)
∈ ℕ0 → ((1..^(♯‘𝐹)) = ∅ ↔ (♯‘𝐹) ≤ 1)) |
60 | | nn0re 11508 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℝ) |
61 | | 1red 10261 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐹)
∈ ℕ0 → 1 ∈ ℝ) |
62 | 60, 61 | jca 501 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝐹) ∈ ℝ ∧ 1 ∈
ℝ)) |
63 | | lenlt 10322 |
. . . . . . . . . . . . . . . 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 2958 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → (1 < (♯‘𝐹) → (1..^(♯‘𝐹)) ≠
∅)) |
68 | 67 | impcom 394 |
. . . . . . . . . . 11
⊢ ((1 <
(♯‘𝐹) ∧
(♯‘𝐹) ∈
ℕ0) → (1..^(♯‘𝐹)) ≠ ∅) |
69 | | rspn0 4082 |
. . . . . . . . . . 11
⊢
((1..^(♯‘𝐹)) ≠ ∅ → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((1 <
(♯‘𝐹) ∧
(♯‘𝐹) ∈
ℕ0) → (∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ 2 → 𝑆 ≤ 2)) |
71 | 70 | ex 397 |
. . . . . . . . 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 1128 |
. . . 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 1105 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (♯‘𝐹)) → 𝑆 ≤ 2) |