Proof of Theorem wlkiswwlks2lem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wlkiswwlks2lem.f | . . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) | 
| 2 | 1 | wlkiswwlks2lem1 29889 | . . 3
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1)) | 
| 3 | 2 | 3adant1 1131 | . 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1)) | 
| 4 |  | lencl 14571 | . . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈
ℕ0) | 
| 5 | 4 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝑃) ∈
ℕ0) | 
| 6 | 1 | wlkiswwlks2lem2 29890 | . . . . . . . . 9
⊢
(((♯‘𝑃)
∈ ℕ0 ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 7 | 5, 6 | sylan 580 | . . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 8 | 7 | adantr 480 | . . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 9 | 8 | fveq2d 6910 | . . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | 
| 10 |  | wlkiswwlks2lem.e | . . . . . . . . . . 11
⊢ 𝐸 = (iEdg‘𝐺) | 
| 11 | 10 | uspgrf1oedg 29190 | . . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) | 
| 12 | 10 | rneqi 5948 | . . . . . . . . . . . 12
⊢ ran 𝐸 = ran (iEdg‘𝐺) | 
| 13 |  | edgval 29066 | . . . . . . . . . . . 12
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) | 
| 14 | 12, 13 | eqtr4i 2768 | . . . . . . . . . . 11
⊢ ran 𝐸 = (Edg‘𝐺) | 
| 15 |  | f1oeq3 6838 | . . . . . . . . . . 11
⊢ (ran
𝐸 = (Edg‘𝐺) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . . . . . 10
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) | 
| 17 | 11, 16 | sylibr 234 | . . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) | 
| 18 | 17 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) | 
| 19 | 18 | adantr 480 | . . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) | 
| 20 |  | f1ocnvfv2 7297 | . . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) | 
| 21 | 19, 20 | sylan 580 | . . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) | 
| 22 | 9, 21 | eqtrd 2777 | . . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) | 
| 23 | 22 | ex 412 | . . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 24 | 23 | ralimdva 3167 | . . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 25 |  | oveq2 7439 | . . . . 5
⊢
((♯‘𝐹) =
((♯‘𝑃) −
1) → (0..^(♯‘𝐹)) = (0..^((♯‘𝑃) − 1))) | 
| 26 | 25 | raleqdv 3326 | . . . 4
⊢
((♯‘𝐹) =
((♯‘𝑃) −
1) → (∀𝑖 ∈
(0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 27 | 26 | imbi2d 340 | . . 3
⊢
((♯‘𝐹) =
((♯‘𝑃) −
1) → ((∀𝑖
∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | 
| 28 | 24, 27 | imbitrrid 246 | . 2
⊢
((♯‘𝐹) =
((♯‘𝑃) −
1) → ((𝐺 ∈
USPGraph ∧ 𝑃 ∈
Word 𝑉 ∧ 1 ≤
(♯‘𝑃)) →
(∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | 
| 29 | 3, 28 | mpcom 38 | 1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |