Step | Hyp | Ref
| Expression |
1 | | df-upwlks 45296 |
. 2
⊢ UPWalks =
(𝑔 ∈ V ↦
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom
(iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈
(0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
2 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) |
3 | | upwlksfval.i |
. . . . . . . 8
⊢ 𝐼 = (iEdg‘𝐺) |
4 | 2, 3 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = 𝐼) |
5 | 4 | dmeqd 5814 |
. . . . . 6
⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = dom 𝐼) |
6 | | wrdeq 14239 |
. . . . . 6
⊢ (dom
(iEdg‘𝑔) = dom 𝐼 → Word dom
(iEdg‘𝑔) = Word dom
𝐼) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑔 = 𝐺 → Word dom (iEdg‘𝑔) = Word dom 𝐼) |
8 | 7 | eleq2d 2824 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑓 ∈ Word dom (iEdg‘𝑔) ↔ 𝑓 ∈ Word dom 𝐼)) |
9 | | fveq2 6774 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
10 | | upwlksfval.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
11 | 9, 10 | eqtr4di 2796 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
12 | 11 | feq3d 6587 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ↔ 𝑝:(0...(♯‘𝑓))⟶𝑉)) |
13 | 4 | fveq1d 6776 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) |
14 | 13 | eqeq1d 2740 |
. . . . 5
⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
15 | 14 | ralbidv 3112 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
16 | 8, 12, 15 | 3anbi123d 1435 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
17 | 16 | opabbidv 5140 |
. 2
⊢ (𝑔 = 𝐺 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
18 | | elex 3450 |
. 2
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
19 | | 3anass 1094 |
. . . 4
⊢ ((𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
20 | 19 | opabbii 5141 |
. . 3
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} |
21 | 3 | fvexi 6788 |
. . . . . 6
⊢ 𝐼 ∈ V |
22 | 21 | dmex 7758 |
. . . . 5
⊢ dom 𝐼 ∈ V |
23 | | wrdexg 14227 |
. . . . 5
⊢ (dom
𝐼 ∈ V → Word dom
𝐼 ∈
V) |
24 | 22, 23 | mp1i 13 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → Word dom 𝐼 ∈ V) |
25 | | ovex 7308 |
. . . . . 6
⊢
(0...(♯‘𝑓)) ∈ V |
26 | 10 | fvexi 6788 |
. . . . . . 7
⊢ 𝑉 ∈ V |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → 𝑉 ∈ V) |
28 | | mapex 8621 |
. . . . . 6
⊢
(((0...(♯‘𝑓)) ∈ V ∧ 𝑉 ∈ V) → {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} ∈ V) |
29 | 25, 27, 28 | sylancr 587 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} ∈ V) |
30 | | simpl 483 |
. . . . . . 7
⊢ ((𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) → 𝑝:(0...(♯‘𝑓))⟶𝑉) |
31 | 30 | ss2abi 4000 |
. . . . . 6
⊢ {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} |
32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉}) |
33 | 29, 32 | ssexd 5248 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
34 | 24, 33 | opabex3d 7808 |
. . 3
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} ∈ V) |
35 | 20, 34 | eqeltrid 2843 |
. 2
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
36 | 1, 17, 18, 35 | fvmptd3 6898 |
1
⊢ (𝐺 ∈ 𝑊 → (UPWalks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |