| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-upwlks 48050 | . 2
⊢ UPWalks =
(𝑔 ∈ V ↦
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom
(iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈
(0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | 
| 2 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) | 
| 3 |  | upwlksfval.i | . . . . . . . 8
⊢ 𝐼 = (iEdg‘𝐺) | 
| 4 | 2, 3 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = 𝐼) | 
| 5 | 4 | dmeqd 5916 | . . . . . 6
⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = dom 𝐼) | 
| 6 |  | wrdeq 14574 | . . . . . 6
⊢ (dom
(iEdg‘𝑔) = dom 𝐼 → Word dom
(iEdg‘𝑔) = Word dom
𝐼) | 
| 7 | 5, 6 | syl 17 | . . . . 5
⊢ (𝑔 = 𝐺 → Word dom (iEdg‘𝑔) = Word dom 𝐼) | 
| 8 | 7 | eleq2d 2827 | . . . 4
⊢ (𝑔 = 𝐺 → (𝑓 ∈ Word dom (iEdg‘𝑔) ↔ 𝑓 ∈ Word dom 𝐼)) | 
| 9 |  | fveq2 6906 | . . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) | 
| 10 |  | upwlksfval.v | . . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) | 
| 11 | 9, 10 | eqtr4di 2795 | . . . . 5
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) | 
| 12 | 11 | feq3d 6723 | . . . 4
⊢ (𝑔 = 𝐺 → (𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ↔ 𝑝:(0...(♯‘𝑓))⟶𝑉)) | 
| 13 | 4 | fveq1d 6908 | . . . . . 6
⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) | 
| 14 | 13 | eqeq1d 2739 | . . . . 5
⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) | 
| 15 | 14 | ralbidv 3178 | . . . 4
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) | 
| 16 | 8, 12, 15 | 3anbi123d 1438 | . . 3
⊢ (𝑔 = 𝐺 → ((𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) | 
| 17 | 16 | opabbidv 5209 | . 2
⊢ (𝑔 = 𝐺 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | 
| 18 |  | elex 3501 | . 2
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) | 
| 19 |  | 3anass 1095 | . . . 4
⊢ ((𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) | 
| 20 | 19 | opabbii 5210 | . . 3
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} | 
| 21 | 3 | fvexi 6920 | . . . . . 6
⊢ 𝐼 ∈ V | 
| 22 | 21 | dmex 7931 | . . . . 5
⊢ dom 𝐼 ∈ V | 
| 23 |  | wrdexg 14562 | . . . . 5
⊢ (dom
𝐼 ∈ V → Word dom
𝐼 ∈
V) | 
| 24 | 22, 23 | mp1i 13 | . . . 4
⊢ (𝐺 ∈ 𝑊 → Word dom 𝐼 ∈ V) | 
| 25 |  | ovex 7464 | . . . . . 6
⊢
(0...(♯‘𝑓)) ∈ V | 
| 26 | 10 | fvexi 6920 | . . . . . . 7
⊢ 𝑉 ∈ V | 
| 27 | 26 | a1i 11 | . . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → 𝑉 ∈ V) | 
| 28 |  | mapex 7963 | . . . . . 6
⊢
(((0...(♯‘𝑓)) ∈ V ∧ 𝑉 ∈ V) → {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} ∈ V) | 
| 29 | 25, 27, 28 | sylancr 587 | . . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} ∈ V) | 
| 30 |  | simpl 482 | . . . . . . 7
⊢ ((𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) → 𝑝:(0...(♯‘𝑓))⟶𝑉) | 
| 31 | 30 | ss2abi 4067 | . . . . . 6
⊢ {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉} | 
| 32 | 31 | a1i 11 | . . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(♯‘𝑓))⟶𝑉}) | 
| 33 | 29, 32 | ssexd 5324 | . . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) | 
| 34 | 24, 33 | opabex3d 7990 | . . 3
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} ∈ V) | 
| 35 | 20, 34 | eqeltrid 2845 | . 2
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) | 
| 36 | 1, 17, 18, 35 | fvmptd3 7039 | 1
⊢ (𝐺 ∈ 𝑊 → (UPWalks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |