Step | Hyp | Ref
| Expression |
1 | | df-wlk 26036 |
. . . 4
⊢ Walks =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
2 | | vex 3176 |
. . . . 5
⊢ 𝑣 ∈ V |
3 | | vex 3176 |
. . . . 5
⊢ 𝑒 ∈ V |
4 | | wlks 26047 |
. . . . . 6
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → (𝑣 Walks 𝑒) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
5 | | ovex 6577 |
. . . . . 6
⊢ (𝑣 Walks 𝑒) ∈ V |
6 | 4, 5 | syl6eqelr 2697 |
. . . . 5
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
7 | 2, 3, 6 | mp2an 704 |
. . . 4
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V |
8 | | dmeq 5246 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → dom 𝑒 = dom 𝐸) |
9 | | wrdeq 13182 |
. . . . . . . . 9
⊢ (dom
𝑒 = dom 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
11 | 10 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → (𝑓 ∈ Word dom 𝑒 ↔ 𝑓 ∈ Word dom 𝐸)) |
12 | 11 | adantl 481 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓 ∈ Word dom 𝑒 ↔ 𝑓 ∈ Word dom 𝐸)) |
13 | | feq3 5941 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
15 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
17 | 16 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
18 | 17 | ralbidv 2969 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
19 | 12, 14, 18 | 3anbi123d 1391 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
20 | 19 | opabbidv 4648 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
21 | 1, 7, 20 | elovmpt2 6777 |
. . 3
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) ↔ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
22 | | elopaelxp 5114 |
. . . 4
⊢ (𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} → 𝑊 ∈ (V × V)) |
23 | | wlkcomp.1 |
. . . . . 6
⊢ 𝐹 = (1st ‘𝑊) |
24 | | wlkcomp.2 |
. . . . . 6
⊢ 𝑃 = (2nd ‘𝑊) |
25 | 23, 24 | wlkcomp 26053 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ (V × V)) →
(𝑊 ∈ (𝑉 Walks 𝐸) ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
26 | 25 | biimpd 218 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ (V × V)) →
(𝑊 ∈ (𝑉 Walks 𝐸) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
27 | 22, 26 | syl3an3 1353 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) → (𝑊 ∈ (𝑉 Walks 𝐸) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
28 | 21, 27 | sylbi 206 |
. 2
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (𝑊 ∈ (𝑉 Walks 𝐸) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
29 | 28 | pm2.43i 50 |
1
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |