Step | Hyp | Ref
| Expression |
1 | | eqid 2740 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
2 | 1 | ewlkprop 27960 |
. . 3
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*)
∧ 𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
3 | | simpl2 1191 |
. . . . 5
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
4 | | xnn0xr 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈
ℕ0* → 𝑇 ∈
ℝ*) |
5 | 4 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
ℕ0* ∧ 𝑇 ∈ ℕ0*)
→ 𝑇 ∈
ℝ*) |
6 | | xnn0xr 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
ℕ0* → 𝑆 ∈
ℝ*) |
7 | 6 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
ℕ0* ∧ 𝑇 ∈ ℕ0*)
→ 𝑆 ∈
ℝ*) |
8 | | fvex 6782 |
. . . . . . . . . . . . . . . 16
⊢
((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∈ V |
9 | 8 | inex1 5245 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V |
10 | | hashxrcl 14062 |
. . . . . . . . . . . . . . 15
⊢
((((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∈ V →
(♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈
ℕ0* ∧ 𝑇 ∈ ℕ0*)
→ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈
ℝ*) |
12 | | xrletr 12883 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ ℝ*
∧ 𝑆 ∈
ℝ* ∧ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) ∈ ℝ*) →
((𝑇 ≤ 𝑆 ∧ 𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → 𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
13 | 5, 7, 11, 12 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈
ℕ0* ∧ 𝑇 ∈ ℕ0*)
→ ((𝑇 ≤ 𝑆 ∧ 𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → 𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
14 | 13 | exp4b 431 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
ℕ0* → (𝑇 ∈ ℕ0*
→ (𝑇 ≤ 𝑆 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))))) |
15 | 14 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝑇 ∈ ℕ0*
→ (𝑇 ≤ 𝑆 → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))))) |
16 | 15 | imp32 419 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → (𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
17 | 16 | ralimdv 3106 |
. . . . . . . . 9
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
18 | 17 | ex 413 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → ((𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))))) |
19 | 18 | com23 86 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))))) |
20 | 19 | a1d 25 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) → (𝐹 ∈ Word dom (iEdg‘𝐺) → (∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))))) |
21 | 20 | 3imp1 1346 |
. . . . 5
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → ∀𝑘 ∈
(1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) |
22 | | simpl1l 1223 |
. . . . . 6
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → 𝐺 ∈ V) |
23 | | simprl 768 |
. . . . . 6
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → 𝑇 ∈
ℕ0*) |
24 | 1 | isewlk 27959 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑇 ∈
ℕ0* ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (𝐹 ∈ (𝐺 EdgWalks 𝑇) ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))))) |
25 | 22, 23, 3, 24 | syl3anc 1370 |
. . . . 5
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → (𝐹 ∈ (𝐺 EdgWalks 𝑇) ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑇 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))))) |
26 | 3, 21, 25 | mpbir2and 710 |
. . . 4
⊢ ((((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) ∧ (𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆)) → 𝐹 ∈ (𝐺 EdgWalks 𝑇)) |
27 | 26 | ex 413 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝑆 ∈
ℕ0*) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺) ∧ ∀𝑘 ∈
(1..^(♯‘𝐹))𝑆 ≤ (♯‘(((iEdg‘𝐺)‘(𝐹‘(𝑘 − 1))) ∩ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → ((𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇))) |
28 | 2, 27 | syl 17 |
. 2
⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇))) |
29 | 28 | 3impib 1115 |
1
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0*
∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇)) |