| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . 3
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 3 | 1, 2 | iswwlks 29856 |
. 2
⊢ (𝑃 ∈ (WWalks‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 4 | | edgval 29066 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 5 | 4 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
| 6 | | upgruhgr 29119 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
| 7 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 8 | 7 | uhgrfun 29083 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
| 9 | 6, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → Fun
(iEdg‘𝐺)) |
| 11 | | elrnrexdm 7109 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝐺) →
({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥))) |
| 12 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥)) |
| 13 | 12 | rexbii 3094 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∃𝑥 ∈ dom (iEdg‘𝐺){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘𝑥)) |
| 14 | 11, 13 | imbitrrdi 252 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝐺) →
({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 15 | 10, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 16 | 5, 15 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 17 | 16 | ralimdv 3169 |
. . . . . . . . . 10
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 18 | 17 | ex 412 |
. . . . . . . . 9
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝐺 ∈ UPGraph → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 19 | 18 | com23 86 |
. . . . . . . 8
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝐺 ∈ UPGraph → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))∃𝑥 ∈
dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 20 | 19 | 3impia 1118 |
. . . . . . 7
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝐺 ∈ UPGraph → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))∃𝑥 ∈
dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 21 | 20 | impcom 407 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))∃𝑥 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
| 22 | | ovex 7464 |
. . . . . . 7
⊢
(0..^((♯‘𝑃) − 1)) ∈ V |
| 23 | | fvex 6919 |
. . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V |
| 24 | 23 | dmex 7931 |
. . . . . . 7
⊢ dom
(iEdg‘𝐺) ∈
V |
| 25 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑥 = (𝑓‘𝑖) → (((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 26 | 22, 24, 25 | ac6 10520 |
. . . . . 6
⊢
(∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))∃𝑥 ∈
dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑥) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∃𝑓(𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 27 | 21, 26 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓(𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 28 | | iswrdi 14556 |
. . . . . . . . . 10
⊢ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑓 ∈ Word dom
(iEdg‘𝐺)) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑓 ∈ Word dom (iEdg‘𝐺)) |
| 30 | 29 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝑓 ∈ Word dom (iEdg‘𝐺)) |
| 31 | | len0nnbi 14589 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 ≠ ∅ ↔ (♯‘𝑃) ∈
ℕ)) |
| 32 | 31 | biimpac 478 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (♯‘𝑃) ∈
ℕ) |
| 33 | | wrdf 14557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → 𝑃:(0..^(♯‘𝑃))⟶(Vtx‘𝐺)) |
| 34 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑃)
∈ ℕ → (♯‘𝑃) ∈ ℤ) |
| 35 | | fzoval 13700 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑃)
∈ ℤ → (0..^(♯‘𝑃)) = (0...((♯‘𝑃) − 1))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑃)
∈ ℕ → (0..^(♯‘𝑃)) = (0...((♯‘𝑃) − 1))) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) →
(0..^(♯‘𝑃)) =
(0...((♯‘𝑃)
− 1))) |
| 38 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑃)
∈ ℕ → ((♯‘𝑃) − 1) ∈
ℕ0) |
| 39 | | fnfzo0hash 14489 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((♯‘𝑃)
− 1) ∈ ℕ0 ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (♯‘𝑓) = ((♯‘𝑃) − 1)) |
| 40 | 38, 39 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (♯‘𝑓) = ((♯‘𝑃) − 1)) |
| 41 | 40 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → ((♯‘𝑃) − 1) =
(♯‘𝑓)) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) →
(0...((♯‘𝑃)
− 1)) = (0...(♯‘𝑓))) |
| 43 | 37, 42 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) →
(0..^(♯‘𝑃)) =
(0...(♯‘𝑓))) |
| 44 | 43 | feq2d 6722 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (𝑃:(0..^(♯‘𝑃))⟶(Vtx‘𝐺) ↔ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 45 | 44 | biimpcd 249 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃:(0..^(♯‘𝑃))⟶(Vtx‘𝐺) → (((♯‘𝑃) ∈ ℕ ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺)) →
𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 46 | 45 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0..^(♯‘𝑃))⟶(Vtx‘𝐺) → ((♯‘𝑃) ∈ ℕ → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺)))) |
| 47 | 33, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → ((♯‘𝑃) ∈ ℕ → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺)))) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → ((♯‘𝑃) ∈ ℕ → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺)))) |
| 49 | 32, 48 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 50 | 49 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 52 | 51 | com12 32 |
. . . . . . . . . 10
⊢ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) →
((𝐺 ∈ UPGraph ∧
(𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓:(0..^((♯‘𝑃) − 1))⟶dom
(iEdg‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺))) |
| 54 | 53 | impcom 407 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺)) |
| 55 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
| 56 | 32, 40 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) → (♯‘𝑓) = ((♯‘𝑃) − 1)) |
| 57 | 56 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) →
(0..^(♯‘𝑓)) =
(0..^((♯‘𝑃)
− 1))) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) →
(0..^(♯‘𝑓)) =
(0..^((♯‘𝑃)
− 1)))) |
| 59 | 58 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) →
(0..^(♯‘𝑓)) =
(0..^((♯‘𝑃)
− 1)))) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) →
(0..^(♯‘𝑓)) =
(0..^((♯‘𝑃)
− 1)))) |
| 61 | 60 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) →
(0..^(♯‘𝑓)) =
(0..^((♯‘𝑃)
− 1))) |
| 62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (0..^(♯‘𝑓)) = (0..^((♯‘𝑃) − 1))) |
| 63 | 55, 62 | raleqtrrdv 3330 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ 𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺)) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
| 64 | 63 | anasss 466 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
| 65 | 30, 54, 64 | 3jca 1129 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) ∧ (𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 66 | 65 | ex 412 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ((𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 67 | 66 | eximdv 1917 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (∃𝑓(𝑓:(0..^((♯‘𝑃) − 1))⟶dom (iEdg‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 68 | 27, 67 | mpd 15 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
| 69 | 1, 7 | upgriswlk 29659 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑃 ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 70 | 69 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑓(Walks‘𝐺)𝑃 ↔ (𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 71 | 70 | exbidv 1921 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ ∃𝑓(𝑓 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))((iEdg‘𝐺)‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 72 | 68, 71 | mpbird 257 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → ∃𝑓 𝑓(Walks‘𝐺)𝑃) |
| 73 | 72 | ex 412 |
. 2
⊢ (𝐺 ∈ UPGraph → ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
| 74 | 3, 73 | biimtrid 242 |
1
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |