Step |
Hyp |
Ref |
Expression |
0 |
|
cwwspthsnon |
⊢ WSPathsNOn |
1 |
|
vn |
⊢ 𝑛 |
2 |
|
cn0 |
⊢ ℕ0 |
3 |
|
vg |
⊢ 𝑔 |
4 |
|
cvv |
⊢ V |
5 |
|
va |
⊢ 𝑎 |
6 |
|
cvtx |
⊢ Vtx |
7 |
3
|
cv |
⊢ 𝑔 |
8 |
7 6
|
cfv |
⊢ ( Vtx ‘ 𝑔 ) |
9 |
|
vb |
⊢ 𝑏 |
10 |
|
vw |
⊢ 𝑤 |
11 |
5
|
cv |
⊢ 𝑎 |
12 |
1
|
cv |
⊢ 𝑛 |
13 |
|
cwwlksnon |
⊢ WWalksNOn |
14 |
12 7 13
|
co |
⊢ ( 𝑛 WWalksNOn 𝑔 ) |
15 |
9
|
cv |
⊢ 𝑏 |
16 |
11 15 14
|
co |
⊢ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) |
17 |
|
vf |
⊢ 𝑓 |
18 |
17
|
cv |
⊢ 𝑓 |
19 |
|
cspthson |
⊢ SPathsOn |
20 |
7 19
|
cfv |
⊢ ( SPathsOn ‘ 𝑔 ) |
21 |
11 15 20
|
co |
⊢ ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) |
22 |
10
|
cv |
⊢ 𝑤 |
23 |
18 22 21
|
wbr |
⊢ 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 |
24 |
23 17
|
wex |
⊢ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 |
25 |
24 10 16
|
crab |
⊢ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } |
26 |
5 9 8 8 25
|
cmpo |
⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) |
27 |
1 3 2 4 26
|
cmpo |
⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) ) |
28 |
0 27
|
wceq |
⊢ WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) ) |