| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elex 3185 |
. 2
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
| 2 | | elex 3185 |
. 2
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
| 3 | | df-wlk 26036 |
. . . 4
⊢ Walks =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
| 4 | 3 | a1i 11 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Walks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})) |
| 5 | | dmeq 5246 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → dom 𝑒 = dom 𝐸) |
| 6 | | wrdeq 13182 |
. . . . . . . 8
⊢ (dom
𝑒 = dom 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
| 7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → Word dom 𝑒 = Word dom 𝐸) |
| 8 | 7 | ad2antll 761 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → Word dom 𝑒 = Word dom 𝐸) |
| 9 | 8 | eleq2d 2673 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑓 ∈ Word dom 𝑒 ↔ 𝑓 ∈ Word dom 𝐸)) |
| 10 | | feq3 5941 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
| 12 | 11 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑝:(0...(#‘𝑓))⟶𝑣 ↔ 𝑝:(0...(#‘𝑓))⟶𝑉)) |
| 13 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
| 14 | 13 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → ((𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ (𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
| 15 | 14 | ralbidv 2969 |
. . . . . 6
⊢ (𝑒 = 𝐸 → (∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
| 16 | 15 | ad2antll 761 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})) |
| 17 | 9, 12, 16 | 3anbi123d 1391 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → ((𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
| 18 | 17 | opabbidv 4648 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
| 19 | | simpl 472 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝑉 ∈ V) |
| 20 | | simpr 476 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
| 21 | | 3anass 1035 |
. . . . 5
⊢ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) ↔ (𝑓 ∈ Word dom 𝐸 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))) |
| 22 | 21 | opabbii 4649 |
. . . 4
⊢
{⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} |
| 23 | | dmexg 6989 |
. . . . . . 7
⊢ (𝐸 ∈ V → dom 𝐸 ∈ V) |
| 24 | 23 | adantl 481 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → dom 𝐸 ∈ V) |
| 25 | | wrdexg 13170 |
. . . . . 6
⊢ (dom
𝐸 ∈ V → Word dom
𝐸 ∈
V) |
| 26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Word dom 𝐸 ∈ V) |
| 27 | | fzfi 12633 |
. . . . . . 7
⊢
(0...(#‘𝑓))
∈ Fin |
| 28 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑓 ∈ Word dom 𝐸) → 𝑉 ∈ V) |
| 29 | | mapex 7750 |
. . . . . . 7
⊢
(((0...(#‘𝑓))
∈ Fin ∧ 𝑉 ∈
V) → {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
| 30 | 27, 28, 29 | sylancr 694 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑓 ∈ Word dom 𝐸) → {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} ∈ V) |
| 31 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) → 𝑝:(0...(#‘𝑓))⟶𝑉) |
| 32 | 31 | ss2abi 3637 |
. . . . . . 7
⊢ {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉} |
| 33 | 32 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑓 ∈ Word dom 𝐸) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ⊆ {𝑝 ∣ 𝑝:(0...(#‘𝑓))⟶𝑉}) |
| 34 | 30, 33 | ssexd 4733 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑓 ∈ Word dom 𝐸) → {𝑝 ∣ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
| 35 | 26, 34 | opabex3d 7037 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}))} ∈ V) |
| 36 | 22, 35 | syl5eqel 2692 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} ∈ V) |
| 37 | 4, 18, 19, 20, 36 | ovmpt2d 6686 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 Walks 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
| 38 | 1, 2, 37 | syl2an 493 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Walks 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
