Step | Hyp | Ref
| Expression |
1 | | df-wlk 26036 |
. . 3
⊢ Walks =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
2 | | vex 3176 |
. . . 4
⊢ 𝑣 ∈ V |
3 | | vex 3176 |
. . . 4
⊢ 𝑒 ∈ V |
4 | | wlks 26047 |
. . . . 5
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → (𝑣 Walks 𝑒) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
5 | | ovex 6577 |
. . . . 5
⊢ (𝑣 Walks 𝑒) ∈ V |
6 | 4, 5 | syl6eqelr 2697 |
. . . 4
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
7 | 2, 3, 6 | mp2an 704 |
. . 3
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V |
8 | | dmeq 5246 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → dom 𝑒 = dom 𝐸) |
9 | | wrdeq 13182 |
. . . . . . . 8
⊢ (dom
𝑒 = dom 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
11 | 10 | eleq2d 2673 |
. . . . . 6
⊢ (𝑒 = 𝐸 → (𝑓 ∈ Word dom 𝑒 ↔ 𝑓 ∈ Word dom 𝐸)) |
12 | 11 | adantl 481 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓 ∈ Word dom 𝑒 ↔ 𝑓 ∈ Word dom 𝐸)) |
13 | | feq3 5941 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
15 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
17 | 16 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
18 | 17 | ralbidv 2969 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
19 | 12, 14, 18 | 3anbi123d 1391 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
20 | 19 | opabbidv 4648 |
. . 3
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
21 | 1, 7, 20 | elovmpt2 6777 |
. 2
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) ↔ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
22 | | eleq1 2676 |
. . . . . 6
⊢ (𝑓 = (1st ‘𝑊) → (𝑓 ∈ Word dom 𝐸 ↔ (1st ‘𝑊) ∈ Word dom 𝐸)) |
23 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑓 = (1st ‘𝑊) → (#‘𝑓) = (#‘(1st
‘𝑊))) |
24 | 23 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑓 = (1st ‘𝑊) → (0...(#‘𝑓)) =
(0...(#‘(1st ‘𝑊)))) |
25 | 24 | feq2d 5944 |
. . . . . 6
⊢ (𝑓 = (1st ‘𝑊) → (𝑝:(0...(#‘𝑓))⟶𝑉 ↔ 𝑝:(0...(#‘(1st ‘𝑊)))⟶𝑉)) |
26 | 23 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑓 = (1st ‘𝑊) → (0..^(#‘𝑓)) =
(0..^(#‘(1st ‘𝑊)))) |
27 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑓 = (1st ‘𝑊) → (𝑓‘𝑘) = ((1st ‘𝑊)‘𝑘)) |
28 | 27 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑓 = (1st ‘𝑊) → (𝐸‘(𝑓‘𝑘)) = (𝐸‘((1st ‘𝑊)‘𝑘))) |
29 | 28 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑓 = (1st ‘𝑊) → ((𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘((1st ‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
30 | 26, 29 | raleqbidv 3129 |
. . . . . 6
⊢ (𝑓 = (1st ‘𝑊) → (∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
31 | 22, 25, 30 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑓 = (1st ‘𝑊) → ((𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘(1st ‘𝑊)))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
32 | | feq1 5939 |
. . . . . 6
⊢ (𝑝 = (2nd ‘𝑊) → (𝑝:(0...(#‘(1st ‘𝑊)))⟶𝑉 ↔ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉)) |
33 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑊) → (𝑝‘𝑘) = ((2nd ‘𝑊)‘𝑘)) |
34 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑊) → (𝑝‘(𝑘 + 1)) = ((2nd ‘𝑊)‘(𝑘 + 1))) |
35 | 33, 34 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑝 = (2nd ‘𝑊) → {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} = {((2nd ‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))}) |
36 | 35 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑝 = (2nd ‘𝑊) → ((𝐸‘((1st ‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘((1st ‘𝑊)‘𝑘)) = {((2nd ‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))})) |
37 | 36 | ralbidv 2969 |
. . . . . 6
⊢ (𝑝 = (2nd ‘𝑊) → (∀𝑘 ∈
(0..^(#‘(1st ‘𝑊)))(𝐸‘((1st ‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {((2nd
‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))})) |
38 | 32, 37 | 3anbi23d 1394 |
. . . . 5
⊢ (𝑝 = (2nd ‘𝑊) → (((1st
‘𝑊) ∈ Word dom
𝐸 ∧ 𝑝:(0...(#‘(1st ‘𝑊)))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {((2nd
‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))}))) |
39 | 31, 38 | elopabi 7120 |
. . . 4
⊢ (𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} → ((1st
‘𝑊) ∈ Word dom
𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘(1st
‘𝑊)))(𝐸‘((1st
‘𝑊)‘𝑘)) = {((2nd
‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))})) |
40 | | 3simpa 1051 |
. . . 4
⊢
(((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st
‘𝑊)))⟶𝑉 ∧ ∀𝑘 ∈
(0..^(#‘(1st ‘𝑊)))(𝐸‘((1st ‘𝑊)‘𝑘)) = {((2nd ‘𝑊)‘𝑘), ((2nd ‘𝑊)‘(𝑘 + 1))}) → ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) |
41 | 39, 40 | syl 17 |
. . 3
⊢ (𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} → ((1st
‘𝑊) ∈ Word dom
𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) |
42 | 41 | 3ad2ant3 1077 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) → ((1st
‘𝑊) ∈ Word dom
𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) |
43 | 21, 42 | sylbi 206 |
1
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) |