Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
2 | | ovex 6577 |
. . . 4
⊢ (𝑉 ClWWalks 𝐸) ∈ V |
3 | | rabexg 4739 |
. . . 4
⊢ ((𝑉 ClWWalks 𝐸) ∈ V → {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁} ∈ V) |
4 | 2, 3 | mp1i 13 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁} ∈ V) |
5 | | eqeq2 2621 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((#‘𝑤) = 𝑛 ↔ (#‘𝑤) = 𝑁)) |
6 | 5 | rabbidv 3164 |
. . . 4
⊢ (𝑛 = 𝑁 → {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛} = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁}) |
7 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) |
8 | 6, 7 | fvmptg 6189 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁} ∈ V) → ((𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁}) |
9 | 1, 4, 8 | syl2anc 691 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁}) |
10 | | df-clwwlkn 26280 |
. . . . . . 7
⊢
ClWWalksN = (𝑣 ∈ V,
𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛})) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ClWWalksN = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}))) |
12 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 ClWWalks 𝑒) = (𝑉 ClWWalks 𝐸)) |
13 | | rabeq 3166 |
. . . . . . . . 9
⊢ ((𝑣 ClWWalks 𝑒) = (𝑉 ClWWalks 𝐸) → {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛} = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛} = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) |
15 | 14 | mpteq2dv 4673 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
17 | | elex 3185 |
. . . . . . 7
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝑉 ∈ V) |
19 | | elex 3185 |
. . . . . . 7
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ∈ V) |
21 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
22 | 21 | mptex 6390 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) ∈ V |
23 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) ∈ V) |
24 | 11, 16, 18, 20, 23 | ovmpt2d 6686 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWWalksN 𝐸) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
25 | 24 | fveq1d 6105 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = ((𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})‘𝑁)) |
26 | 25 | eqeq1d 2612 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁} ↔ ((𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁})) |
27 | 26 | 3adant3 1074 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁} ↔ ((𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁})) |
28 | 9, 27 | mpbird 246 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁}) |