Detailed syntax breakdown of Definition df-plpq
Step | Hyp | Ref
| Expression |
1 | | cplpq 7209 |
. 2
class
+pQ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cnpi 7205 |
. . . 4
class
N |
5 | 4, 4 | cxp 4597 |
. . 3
class
(N × N) |
6 | 2 | cv 1341 |
. . . . . . 7
class 𝑥 |
7 | | c1st 6099 |
. . . . . . 7
class
1st |
8 | 6, 7 | cfv 5183 |
. . . . . 6
class
(1st ‘𝑥) |
9 | 3 | cv 1341 |
. . . . . . 7
class 𝑦 |
10 | | c2nd 6100 |
. . . . . . 7
class
2nd |
11 | 9, 10 | cfv 5183 |
. . . . . 6
class
(2nd ‘𝑦) |
12 | | cmi 7207 |
. . . . . 6
class
·N |
13 | 8, 11, 12 | co 5837 |
. . . . 5
class
((1st ‘𝑥) ·N
(2nd ‘𝑦)) |
14 | 9, 7 | cfv 5183 |
. . . . . 6
class
(1st ‘𝑦) |
15 | 6, 10 | cfv 5183 |
. . . . . 6
class
(2nd ‘𝑥) |
16 | 14, 15, 12 | co 5837 |
. . . . 5
class
((1st ‘𝑦) ·N
(2nd ‘𝑥)) |
17 | | cpli 7206 |
. . . . 5
class
+N |
18 | 13, 16, 17 | co 5837 |
. . . 4
class
(((1st ‘𝑥) ·N
(2nd ‘𝑦))
+N ((1st ‘𝑦) ·N
(2nd ‘𝑥))) |
19 | 15, 11, 12 | co 5837 |
. . . 4
class
((2nd ‘𝑥) ·N
(2nd ‘𝑦)) |
20 | 18, 19 | cop 3574 |
. . 3
class
〈(((1st ‘𝑥) ·N
(2nd ‘𝑦))
+N ((1st ‘𝑦) ·N
(2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉 |
21 | 2, 3, 5, 5, 20 | cmpo 5839 |
. 2
class (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
22 | 1, 21 | wceq 1342 |
1
wff
+pQ = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ 〈(((1st
‘𝑥)
·N (2nd ‘𝑦)) +N
((1st ‘𝑦)
·N (2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |