Proof of Theorem 1wlkiswwlks2lem5
Step | Hyp | Ref
| Expression |
1 | | 1wlkiswwlks2lem.e |
. . . . . . . . 9
⊢ 𝐸 = (iEdg‘𝐺) |
2 | 1 | uspgrf1oedg 40403 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
3 | | edgaval 25794 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
4 | 1 | rneqi 5273 |
. . . . . . . . . 10
⊢ ran 𝐸 = ran (iEdg‘𝐺) |
5 | 3, 4 | syl6reqr 2663 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → ran
𝐸 = (Edg‘𝐺)) |
6 | 5 | f1oeq3d 6047 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) |
7 | 2, 6 | mpbird 246 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
8 | 7 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
9 | 8 | ad2antrr 758 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
10 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → 𝑥 ∈ (0..^((#‘𝑃) − 1))) |
11 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘𝑖) = (𝑃‘𝑥)) |
12 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 + 1) = (𝑥 + 1)) |
13 | 12 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑥 + 1))) |
14 | 11, 13 | preq12d 4220 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
15 | 14 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) ∧ 𝑖 = 𝑥) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
17 | 10, 16 | rspcdv 3285 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
18 | 17 | impancom 455 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑥 ∈ (0..^((#‘𝑃) − 1)) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸)) |
19 | 18 | imp 444 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) |
20 | | f1ocnvdm 6440 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∈ ran 𝐸) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
21 | 9, 19, 20 | syl2anc 691 |
. . . 4
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑥 ∈ (0..^((#‘𝑃) − 1))) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) ∈ dom 𝐸) |
22 | | 1wlkiswwlks2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
23 | 21, 22 | fmptd 6292 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹:(0..^((#‘𝑃) − 1))⟶dom 𝐸) |
24 | | iswrdi 13164 |
. . 3
⊢ (𝐹:(0..^((#‘𝑃) − 1))⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
25 | 23, 24 | syl 17 |
. 2
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → 𝐹 ∈ Word dom 𝐸) |
26 | 25 | ex 449 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) |