Detailed syntax breakdown of Definition df-wspthsnon
Step | Hyp | Ref
| Expression |
1 | | cwwspthsnon 28202 |
. 2
class
WSPathsNOn |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vg |
. . 3
setvar 𝑔 |
4 | | cn0 12243 |
. . 3
class
ℕ0 |
5 | | cvv 3429 |
. . 3
class
V |
6 | | va |
. . . 4
setvar 𝑎 |
7 | | vb |
. . . 4
setvar 𝑏 |
8 | 3 | cv 1538 |
. . . . 5
class 𝑔 |
9 | | cvtx 27376 |
. . . . 5
class
Vtx |
10 | 8, 9 | cfv 6426 |
. . . 4
class
(Vtx‘𝑔) |
11 | | vf |
. . . . . . . 8
setvar 𝑓 |
12 | 11 | cv 1538 |
. . . . . . 7
class 𝑓 |
13 | | vw |
. . . . . . . 8
setvar 𝑤 |
14 | 13 | cv 1538 |
. . . . . . 7
class 𝑤 |
15 | 6 | cv 1538 |
. . . . . . . 8
class 𝑎 |
16 | 7 | cv 1538 |
. . . . . . . 8
class 𝑏 |
17 | | cspthson 28091 |
. . . . . . . . 9
class
SPathsOn |
18 | 8, 17 | cfv 6426 |
. . . . . . . 8
class
(SPathsOn‘𝑔) |
19 | 15, 16, 18 | co 7267 |
. . . . . . 7
class (𝑎(SPathsOn‘𝑔)𝑏) |
20 | 12, 14, 19 | wbr 5073 |
. . . . . 6
wff 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤 |
21 | 20, 11 | wex 1782 |
. . . . 5
wff
∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤 |
22 | 2 | cv 1538 |
. . . . . . 7
class 𝑛 |
23 | | cwwlksnon 28200 |
. . . . . . 7
class
WWalksNOn |
24 | 22, 8, 23 | co 7267 |
. . . . . 6
class (𝑛 WWalksNOn 𝑔) |
25 | 15, 16, 24 | co 7267 |
. . . . 5
class (𝑎(𝑛 WWalksNOn 𝑔)𝑏) |
26 | 21, 13, 25 | crab 3068 |
. . . 4
class {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤} |
27 | 6, 7, 10, 10, 26 | cmpo 7269 |
. . 3
class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}) |
28 | 2, 3, 4, 5, 27 | cmpo 7269 |
. 2
class (𝑛 ∈ ℕ0,
𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤})) |
29 | 1, 28 | wceq 1539 |
1
wff WSPathsNOn
= (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ (𝑎 ∈
(Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤})) |