Step | Hyp | Ref
| Expression |
1 | | df-wwlksn 41034 |
. . . . 5
⊢ WWalkSN
= (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ {𝑤 ∈
(WWalkS‘𝑔) ∣
(#‘𝑤) = (𝑛 + 1)}) |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
WWalkSN = (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ {𝑤 ∈
(WWalkS‘𝑔) ∣
(#‘𝑤) = (𝑛 + 1)})) |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (WWalkS‘𝑔) = (WWalkS‘𝐺)) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑔 = 𝐺) → (WWalkS‘𝑔) = (WWalkS‘𝐺)) |
5 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1)) |
6 | 5 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((#‘𝑤) = (𝑛 + 1) ↔ (#‘𝑤) = (𝑁 + 1))) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑔 = 𝐺) → ((#‘𝑤) = (𝑛 + 1) ↔ (#‘𝑤) = (𝑁 + 1))) |
8 | 4, 7 | rabeqbidv 3168 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑔 = 𝐺) → {𝑤 ∈ (WWalkS‘𝑔) ∣ (#‘𝑤) = (𝑛 + 1)} = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |
9 | 8 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑛 = 𝑁 ∧ 𝑔 = 𝐺)) → {𝑤 ∈ (WWalkS‘𝑔) ∣ (#‘𝑤) = (𝑛 + 1)} = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |
10 | | simpl 472 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
𝑁 ∈
ℕ0) |
11 | | simpr 476 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
𝐺 ∈
V) |
12 | | fvex 6113 |
. . . . . 6
⊢
(WWalkS‘𝐺)
∈ V |
13 | 12 | rabex 4740 |
. . . . 5
⊢ {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} ∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
{𝑤 ∈
(WWalkS‘𝐺) ∣
(#‘𝑤) = (𝑁 + 1)} ∈
V) |
15 | 2, 9, 10, 11, 14 | ovmpt2d 6686 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |
16 | 15 | expcom 450 |
. 2
⊢ (𝐺 ∈ V → (𝑁 ∈ ℕ0
→ (𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)})) |
17 | 1 | reldmmpt2 6669 |
. . . . 5
⊢ Rel dom
WWalkSN |
18 | 17 | ovprc2 6583 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑁 WWalkSN 𝐺) = ∅) |
19 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(WWalkS‘𝐺) =
∅) |
20 | 19 | rabeqdv 3167 |
. . . . 5
⊢ (¬
𝐺 ∈ V → {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} = {𝑤 ∈ ∅ ∣ (#‘𝑤) = (𝑁 + 1)}) |
21 | | rab0 3909 |
. . . . 5
⊢ {𝑤 ∈ ∅ ∣
(#‘𝑤) = (𝑁 + 1)} =
∅ |
22 | 20, 21 | syl6eq 2660 |
. . . 4
⊢ (¬
𝐺 ∈ V → {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} = ∅) |
23 | 18, 22 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐺 ∈ V → (𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |
24 | 23 | a1d 25 |
. 2
⊢ (¬
𝐺 ∈ V → (𝑁 ∈ ℕ0
→ (𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)})) |
25 | 16, 24 | pm2.61i 175 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) |