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