Proof of Theorem wlkiswwlks2lem5
Step | Hyp | Ref
| Expression |
1 | | wlkiswwlks2lem.e |
. . . . . . . . 9
⊢ 𝐸 = (iEdg‘𝐺) |
2 | 1 | uspgrf1oedg 26885 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
3 | 1 | rneqi 5800 |
. . . . . . . . . . 11
⊢ ran 𝐸 = ran (iEdg‘𝐺) |
4 | | edgval 26761 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
5 | 3, 4 | eqtr4i 2844 |
. . . . . . . . . 10
⊢ ran 𝐸 = (Edg‘𝐺) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → ran
𝐸 = (Edg‘𝐺)) |
7 | 6 | f1oeq3d 6605 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) |
8 | 2, 7 | mpbird 258 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
9 | 8 | 3ad2ant1 1125 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
10 | 9 | ad2antrr 722 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
11 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → 𝑥 ∈
(0..^((♯‘𝑃)
− 1))) |
12 | | fveq2 6663 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘𝑖) = (𝑃‘𝑥)) |
13 | | fvoveq1 7168 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑥 + 1))) |
14 | 12, 13 | preq12d 4669 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
15 | 14 | eleq1d 2894 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
16 | 15 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) ∧ 𝑖 = 𝑥) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
17 | 11, 16 | rspcdv 3612 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) →
(∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
18 | 17 | impancom 452 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑥 ∈ (0..^((♯‘𝑃) − 1)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
19 | 18 | imp 407 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) |
20 | | f1ocnvdm 7032 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
21 | 10, 19, 20 | syl2anc 584 |
. . . 4
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((♯‘𝑃) − 1))) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
22 | | wlkiswwlks2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
23 | 21, 22 | fmptd 6870 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹:(0..^((♯‘𝑃) − 1))⟶dom 𝐸) |
24 | | iswrdi 13853 |
. . 3
⊢ (𝐹:(0..^((♯‘𝑃) − 1))⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
25 | 23, 24 | syl 17 |
. 2
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹 ∈ Word dom 𝐸) |
26 | 25 | ex 413 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) |