Detailed syntax breakdown of Definition df-2spthonot
Step | Hyp | Ref
| Expression |
1 | | c2pthonot 26384 |
. 2
class
2SPathOnOt |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | va |
. . . 4
setvar 𝑎 |
6 | | vb |
. . . 4
setvar 𝑏 |
7 | 2 | cv 1474 |
. . . 4
class 𝑣 |
8 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
9 | 8 | cv 1474 |
. . . . . . . . 9
class 𝑓 |
10 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
11 | 10 | cv 1474 |
. . . . . . . . 9
class 𝑝 |
12 | 5 | cv 1474 |
. . . . . . . . . 10
class 𝑎 |
13 | 6 | cv 1474 |
. . . . . . . . . 10
class 𝑏 |
14 | 3 | cv 1474 |
. . . . . . . . . . 11
class 𝑒 |
15 | | cspthon 26033 |
. . . . . . . . . . 11
class
SPathOn |
16 | 7, 14, 15 | co 6549 |
. . . . . . . . . 10
class (𝑣 SPathOn 𝑒) |
17 | 12, 13, 16 | co 6549 |
. . . . . . . . 9
class (𝑎(𝑣 SPathOn 𝑒)𝑏) |
18 | 9, 11, 17 | wbr 4583 |
. . . . . . . 8
wff 𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 |
19 | | chash 12979 |
. . . . . . . . . 10
class
# |
20 | 9, 19 | cfv 5804 |
. . . . . . . . 9
class
(#‘𝑓) |
21 | | c2 10947 |
. . . . . . . . 9
class
2 |
22 | 20, 21 | wceq 1475 |
. . . . . . . 8
wff
(#‘𝑓) =
2 |
23 | | vt |
. . . . . . . . . . . . 13
setvar 𝑡 |
24 | 23 | cv 1474 |
. . . . . . . . . . . 12
class 𝑡 |
25 | | c1st 7057 |
. . . . . . . . . . . 12
class
1st |
26 | 24, 25 | cfv 5804 |
. . . . . . . . . . 11
class
(1st ‘𝑡) |
27 | 26, 25 | cfv 5804 |
. . . . . . . . . 10
class
(1st ‘(1st ‘𝑡)) |
28 | 27, 12 | wceq 1475 |
. . . . . . . . 9
wff
(1st ‘(1st ‘𝑡)) = 𝑎 |
29 | | c2nd 7058 |
. . . . . . . . . . 11
class
2nd |
30 | 26, 29 | cfv 5804 |
. . . . . . . . . 10
class
(2nd ‘(1st ‘𝑡)) |
31 | | c1 9816 |
. . . . . . . . . . 11
class
1 |
32 | 31, 11 | cfv 5804 |
. . . . . . . . . 10
class (𝑝‘1) |
33 | 30, 32 | wceq 1475 |
. . . . . . . . 9
wff
(2nd ‘(1st ‘𝑡)) = (𝑝‘1) |
34 | 24, 29 | cfv 5804 |
. . . . . . . . . 10
class
(2nd ‘𝑡) |
35 | 34, 13 | wceq 1475 |
. . . . . . . . 9
wff
(2nd ‘𝑡) = 𝑏 |
36 | 28, 33, 35 | w3a 1031 |
. . . . . . . 8
wff
((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏) |
37 | 18, 22, 36 | w3a 1031 |
. . . . . . 7
wff (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)) |
38 | 37, 10 | wex 1695 |
. . . . . 6
wff
∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)) |
39 | 38, 8 | wex 1695 |
. . . . 5
wff
∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)) |
40 | 7, 7 | cxp 5036 |
. . . . . 6
class (𝑣 × 𝑣) |
41 | 40, 7 | cxp 5036 |
. . . . 5
class ((𝑣 × 𝑣) × 𝑣) |
42 | 39, 23, 41 | crab 2900 |
. . . 4
class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))} |
43 | 5, 6, 7, 7, 42 | cmpt2 6551 |
. . 3
class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) |
44 | 2, 3, 4, 4, 43 | cmpt2 6551 |
. 2
class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |
45 | 1, 44 | wceq 1475 |
1
wff 2SPathOnOt
= (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |