Step | Hyp | Ref
| Expression |
1 | | df-1wlks 40800 |
. . 3
⊢ 1Walks =
(𝑔 ∈ V ↦
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom
(iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐺 ∈ 𝑊 → 1Walks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))})) |
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 | | biidd 251 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) ↔ (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)))) |
15 | 5 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘(𝑓‘𝑘)) = (𝐼‘(𝑓‘𝑘))) |
16 | 15 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)} ↔ (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)})) |
17 | 15 | sseq2d 3596 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ({(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) ↔ {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))) |
18 | 14, 16, 17 | ifpbi123d 1021 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))) ↔ if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))) |
19 | 18 | ralbidv 2969 |
. . . . 5
⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))) ↔ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))) |
20 | 9, 13, 19 | 3anbi123d 1391 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)))) ↔ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))))) |
21 | 20 | opabbidv 4648 |
. . 3
⊢ (𝑔 = 𝐺 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}) |
22 | 21 | adantl 481 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}) |
23 | | elex 3185 |
. 2
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
24 | | 3anass 1035 |
. . . 4
⊢ ((𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))) ↔ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))))) |
25 | 24 | opabbii 4649 |
. . 3
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))))} |
26 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝐺)
∈ V |
27 | 4, 26 | eqeltri 2684 |
. . . . . 6
⊢ 𝐼 ∈ V |
28 | 27 | dmex 6991 |
. . . . 5
⊢ dom 𝐼 ∈ V |
29 | | wrdexg 13170 |
. . . . 5
⊢ (dom
𝐼 ∈ V → Word dom
𝐼 ∈
V) |
30 | 28, 29 | mp1i 13 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → Word dom 𝐼 ∈ V) |
31 | | ovex 6577 |
. . . . . 6
⊢
(0...(#‘𝑓))
∈ V |
32 | | fvex 6113 |
. . . . . . . 8
⊢
(Vtx‘𝐺) ∈
V |
33 | 11, 32 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑉 ∈ V |
34 | 33 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → 𝑉 ∈ V) |
35 | | mapex 7750 |
. . . . . 6
⊢
(((0...(#‘𝑓))
∈ V ∧ 𝑉 ∈ V)
→ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
36 | 31, 34, 35 | sylancr 694 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
37 | | simpl 472 |
. . . . . . 7
⊢ ((𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))) → 𝑝:(0...(#‘𝑓))⟶𝑉) |
38 | 37 | ss2abi 3637 |
. . . . . 6
⊢ {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} |
39 | 38 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉}) |
40 | 36, 39 | ssexd 4733 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ∈ V) |
41 | 30, 40 | opabex3d 7037 |
. . 3
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))))} ∈ V) |
42 | 25, 41 | syl5eqel 2692 |
. 2
⊢ (𝐺 ∈ 𝑊 → {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ∈ V) |
43 | 2, 22, 23, 42 | fvmptd 6197 |
1
⊢ (𝐺 ∈ 𝑊 → (1Walks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}) |