Detailed syntax breakdown of Definition df-2spthsot
Step | Hyp | Ref
| Expression |
1 | | c2spthot 26383 |
. 2
class
2SPathsOt |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vt |
. . . . . . . 8
setvar 𝑡 |
6 | 5 | cv 1474 |
. . . . . . 7
class 𝑡 |
7 | | va |
. . . . . . . . 9
setvar 𝑎 |
8 | 7 | cv 1474 |
. . . . . . . 8
class 𝑎 |
9 | | vb |
. . . . . . . . 9
setvar 𝑏 |
10 | 9 | cv 1474 |
. . . . . . . 8
class 𝑏 |
11 | 2 | cv 1474 |
. . . . . . . . 9
class 𝑣 |
12 | 3 | cv 1474 |
. . . . . . . . 9
class 𝑒 |
13 | | c2pthonot 26384 |
. . . . . . . . 9
class
2SPathOnOt |
14 | 11, 12, 13 | co 6549 |
. . . . . . . 8
class (𝑣 2SPathOnOt 𝑒) |
15 | 8, 10, 14 | co 6549 |
. . . . . . 7
class (𝑎(𝑣 2SPathOnOt 𝑒)𝑏) |
16 | 6, 15 | wcel 1977 |
. . . . . 6
wff 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏) |
17 | 16, 9, 11 | wrex 2897 |
. . . . 5
wff
∃𝑏 ∈
𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏) |
18 | 17, 7, 11 | wrex 2897 |
. . . 4
wff
∃𝑎 ∈
𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏) |
19 | 11, 11 | cxp 5036 |
. . . . 5
class (𝑣 × 𝑣) |
20 | 19, 11 | cxp 5036 |
. . . 4
class ((𝑣 × 𝑣) × 𝑣) |
21 | 18, 5, 20 | crab 2900 |
. . 3
class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)} |
22 | 2, 3, 4, 4, 21 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)}) |
23 | 1, 22 | wceq 1475 |
1
wff 2SPathsOt
= (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)}) |