Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( WWalks ‘ 𝑔 ) = ( WWalks ‘ 𝐺 ) ) |
2 |
1
|
adantl |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( WWalks ‘ 𝑔 ) = ( WWalks ‘ 𝐺 ) ) |
3 |
|
oveq1 |
⊢ ( 𝑛 = 𝑁 → ( 𝑛 + 1 ) = ( 𝑁 + 1 ) ) |
4 |
3
|
eqeq2d |
⊢ ( 𝑛 = 𝑁 → ( ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) |
6 |
2 5
|
rabeqbidv |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |
7 |
|
df-wwlksn |
⊢ WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } ) |
8 |
|
fvex |
⊢ ( WWalks ‘ 𝐺 ) ∈ V |
9 |
8
|
rabex |
⊢ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ∈ V |
10 |
6 7 9
|
ovmpoa |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |
11 |
10
|
expcom |
⊢ ( 𝐺 ∈ V → ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) ) |
12 |
7
|
reldmmpo |
⊢ Rel dom WWalksN |
13 |
12
|
ovprc2 |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 WWalksN 𝐺 ) = ∅ ) |
14 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = ∅ ) |
15 |
14
|
rabeqdv |
⊢ ( ¬ 𝐺 ∈ V → { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = { 𝑤 ∈ ∅ ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |
16 |
|
rab0 |
⊢ { 𝑤 ∈ ∅ ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = ∅ |
17 |
15 16
|
eqtrdi |
⊢ ( ¬ 𝐺 ∈ V → { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = ∅ ) |
18 |
13 17
|
eqtr4d |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |
19 |
18
|
a1d |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) ) |
20 |
11 19
|
pm2.61i |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |