Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnon.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
df-wspthsnon |
⊢ WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) ) |
3 |
2
|
a1i |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) |
5 |
4 1
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 ) |
6 |
5
|
adantl |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( Vtx ‘ 𝑔 ) = 𝑉 ) |
7 |
|
oveq12 |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑛 WWalksNOn 𝑔 ) = ( 𝑁 WWalksNOn 𝐺 ) ) |
8 |
7
|
oveqd |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) = ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( SPathsOn ‘ 𝑔 ) = ( SPathsOn ‘ 𝐺 ) ) |
10 |
9
|
oveqd |
⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) = ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) ) |
11 |
10
|
breqd |
⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 ↔ 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 ↔ 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 ) ) |
13 |
12
|
exbidv |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 ) ) |
14 |
8 13
|
rabeqbidv |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } = { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) |
15 |
6 6 14
|
mpoeq123dv |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) ) |
17 |
|
simpl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → 𝑁 ∈ ℕ0 ) |
18 |
|
elex |
⊢ ( 𝐺 ∈ 𝑈 → 𝐺 ∈ V ) |
19 |
18
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → 𝐺 ∈ V ) |
20 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
21 |
20 20
|
mpoex |
⊢ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) ∈ V |
22 |
21
|
a1i |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) ∈ V ) |
23 |
3 16 17 19 22
|
ovmpod |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WSPathsNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) ) |