Step | Hyp | Ref
| Expression |
1 | | df-wlks 40801 |
. . 3
⊢ UPWalks =
(𝑔 ∈ V ↦
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom
(iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐺 ∈ 𝑊 → UPWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
3 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) |
4 | | 1wlksfval.i |
. . . . . . . . 9
⊢ 𝐼 = (iEdg‘𝐺) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = 𝐼) |
6 | 5 | dmeqd 5248 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = dom 𝐼) |
7 | | wrdeq 13182 |
. . . . . . 7
⊢ (dom
(iEdg‘𝑔) = dom 𝐼 → Word dom
(iEdg‘𝑔) = Word dom
𝐼) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝑔 = 𝐺 → Word dom (iEdg‘𝑔) = Word dom 𝐼) |
9 | 8 | eleq2d 2673 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑓 ∈ Word dom (iEdg‘𝑔) ↔ 𝑓 ∈ Word dom 𝐼)) |
10 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
11 | | 1wlksfval.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
13 | 12 | feq3d 5945 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
14 | 5 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) |
15 | 14 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
16 | 15 | ralbidv 2969 |
. . . . 5
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
17 | 9, 13, 16 | 3anbi123d 1391 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
18 | 17 | opabbidv 4648 |
. . 3
⊢ (𝑔 = 𝐺 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
19 | 18 | adantl 481 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
20 | | elex 3185 |
. 2
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
21 | | 3anass 1035 |
. . . 4
⊢ ((𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
22 | 21 | opabbii 4649 |
. . 3
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} |
23 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝐺)
∈ V |
24 | 4, 23 | eqeltri 2684 |
. . . . . 6
⊢ 𝐼 ∈ V |
25 | 24 | dmex 6991 |
. . . . 5
⊢ dom 𝐼 ∈ V |
26 | | wrdexg 13170 |
. . . . 5
⊢ (dom
𝐼 ∈ V → Word dom
𝐼 ∈
V) |
27 | 25, 26 | mp1i 13 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → Word dom 𝐼 ∈ V) |
28 | | ovex 6577 |
. . . . . 6
⊢
(0...(#‘𝑓))
∈ V |
29 | | fvex 6113 |
. . . . . . . 8
⊢
(Vtx‘𝐺) ∈
V |
30 | 11, 29 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑉 ∈ V |
31 | 30 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → 𝑉 ∈ V) |
32 | | mapex 7750 |
. . . . . 6
⊢
(((0...(#‘𝑓))
∈ V ∧ 𝑉 ∈ V)
→ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
33 | 28, 31, 32 | sylancr 694 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
34 | | simpl 472 |
. . . . . . 7
⊢ ((𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) → 𝑝:(0...(#‘𝑓))⟶𝑉) |
35 | 34 | ss2abi 3637 |
. . . . . 6
⊢ {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} |
36 | 35 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉}) |
37 | 33, 36 | ssexd 4733 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
38 | 27, 37 | opabex3d 7037 |
. . 3
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} ∈ V) |
39 | 22, 38 | syl5eqel 2692 |
. 2
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
40 | 2, 19, 20, 39 | fvmptd 6197 |
1
⊢ (𝐺 ∈ 𝑊 → (UPWalks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |