Proof of Theorem wlkiswwlks2lem5
Step | Hyp | Ref
| Expression |
1 | | wlkiswwlks2lem.e |
. . . . . . . . 9
⊢ 𝐸 = (iEdg‘𝐺) |
2 | 1 | uspgrf1oedg 26068 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
3 | 1 | rneqi 5352 |
. . . . . . . . . . 11
⊢ ran 𝐸 = ran (iEdg‘𝐺) |
4 | | edgval 25941 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
5 | 3, 4 | eqtr4i 2647 |
. . . . . . . . . 10
⊢ ran 𝐸 = (Edg‘𝐺) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → ran
𝐸 = (Edg‘𝐺)) |
7 | 6 | f1oeq3d 6134 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) |
8 | 2, 7 | mpbird 247 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
9 | 8 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
10 | 9 | ad2antrr 762 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
11 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → 𝑥 ∈ (0..^((#‘𝑃) − 1))) |
12 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘𝑖) = (𝑃‘𝑥)) |
13 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 + 1) = (𝑥 + 1)) |
14 | 13 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑥 + 1))) |
15 | 12, 14 | preq12d 4276 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
16 | 15 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) ∧ 𝑖 = 𝑥) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
18 | 11, 17 | rspcdv 3312 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
19 | 18 | impancom 456 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑥 ∈ (0..^((#‘𝑃) − 1)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
20 | 19 | imp 445 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) |
21 | | f1ocnvdm 6540 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
22 | 10, 20, 21 | syl2anc 693 |
. . . 4
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
23 | | wlkiswwlks2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
24 | 22, 23 | fmptd 6385 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹:(0..^((#‘𝑃) − 1))⟶dom 𝐸) |
25 | | iswrdi 13309 |
. . 3
⊢ (𝐹:(0..^((#‘𝑃) − 1))⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
26 | 24, 25 | syl 17 |
. 2
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹 ∈ Word dom 𝐸) |
27 | 26 | ex 450 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) |