Step | Hyp | Ref
| Expression |
1 | | cmpq 6261 |
. 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 |
. . . . . 6
class x |
7 | | c1st 5707 |
. . . . . 6
class
1^{st} |
8 | 6, 7 | cfv 4845 |
. . . . 5
class (1^{st}
‘x) |
9 | 3 | cv 1241 |
. . . . . 6
class y |
10 | 9, 7 | cfv 4845 |
. . . . 5
class (1^{st}
‘y) |
11 | | cmi 6258 |
. . . . 5
class
·_{N} |
12 | 8, 10, 11 | co 5455 |
. . . 4
class ((1^{st}
‘x)
·_{N} (1^{st} ‘y)) |
13 | | c2nd 5708 |
. . . . . 6
class
2^{nd} |
14 | 6, 13 | cfv 4845 |
. . . . 5
class (2^{nd}
‘x) |
15 | 9, 13 | cfv 4845 |
. . . . 5
class (2^{nd}
‘y) |
16 | 14, 15, 11 | co 5455 |
. . . 4
class ((2^{nd}
‘x)
·_{N} (2^{nd} ‘y)) |
17 | 12, 16 | cop 3370 |
. . 3
class ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩ |
18 | 2, 3, 5, 5, 17 | cmpt2 5457 |
. 2
class (x ∈
(N × N), y ∈
(N × N) ↦ ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |
19 | 1, 18 | wceq 1242 |
1
wff
·_{pQ} = (x
∈ (N × N),
y ∈
(N × N) ↦ ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |