Detailed syntax breakdown of Definition df-plpq
Step | Hyp | Ref
| Expression |
1 | | cplpq 6260 |
. 2
class
+pQ |
2 | | vx |
. . 3
setvar x |
3 | | vy |
. . 3
setvar y |
4 | | cnpi 6256 |
. . . 4
class
N |
5 | 4, 4 | cxp 4286 |
. . 3
class (N ×
N) |
6 | 2 | cv 1241 |
. . . . . . 7
class x |
7 | | c1st 5707 |
. . . . . . 7
class
1st |
8 | 6, 7 | cfv 4845 |
. . . . . 6
class (1st
‘x) |
9 | 3 | cv 1241 |
. . . . . . 7
class y |
10 | | c2nd 5708 |
. . . . . . 7
class
2nd |
11 | 9, 10 | cfv 4845 |
. . . . . 6
class (2nd
‘y) |
12 | | cmi 6258 |
. . . . . 6
class
·N |
13 | 8, 11, 12 | co 5455 |
. . . . 5
class ((1st
‘x)
·N (2nd ‘y)) |
14 | 9, 7 | cfv 4845 |
. . . . . 6
class (1st
‘y) |
15 | 6, 10 | cfv 4845 |
. . . . . 6
class (2nd
‘x) |
16 | 14, 15, 12 | co 5455 |
. . . . 5
class ((1st
‘y)
·N (2nd ‘x)) |
17 | | cpli 6257 |
. . . . 5
class
+N |
18 | 13, 16, 17 | co 5455 |
. . . 4
class (((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))) |
19 | 15, 11, 12 | co 5455 |
. . . 4
class ((2nd
‘x)
·N (2nd ‘y)) |
20 | 18, 19 | cop 3370 |
. . 3
class 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉 |
21 | 2, 3, 5, 5, 20 | cmpt2 5457 |
. 2
class (x ∈
(N × N), y ∈
(N × N) ↦ 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉) |
22 | 1, 21 | wceq 1242 |
1
wff +pQ
= (x ∈
(N × N), y ∈
(N × N) ↦ 〈(((1st
‘x)
·N (2nd ‘y)) +N ((1st
‘y)
·N (2nd ‘x))), ((2nd ‘x) ·N
(2nd ‘y))〉) |