Step | Hyp | Ref
| Expression |
1 | | cmpq 9956 |
. 2
class
·_{pQ} |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cnpi 9951 |
. . . 4
class
N |
5 | 4, 4 | cxp 5309 |
. . 3
class
(N × N) |
6 | 2 | cv 1636 |
. . . . . 6
class 𝑥 |
7 | | c1st 7396 |
. . . . . 6
class
1^{st} |
8 | 6, 7 | cfv 6101 |
. . . . 5
class
(1^{st} ‘𝑥) |
9 | 3 | cv 1636 |
. . . . . 6
class 𝑦 |
10 | 9, 7 | cfv 6101 |
. . . . 5
class
(1^{st} ‘𝑦) |
11 | | cmi 9953 |
. . . . 5
class
·_{N} |
12 | 8, 10, 11 | co 6874 |
. . . 4
class
((1^{st} ‘𝑥) ·_{N}
(1^{st} ‘𝑦)) |
13 | | c2nd 7397 |
. . . . . 6
class
2^{nd} |
14 | 6, 13 | cfv 6101 |
. . . . 5
class
(2^{nd} ‘𝑥) |
15 | 9, 13 | cfv 6101 |
. . . . 5
class
(2^{nd} ‘𝑦) |
16 | 14, 15, 11 | co 6874 |
. . . 4
class
((2^{nd} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦)) |
17 | 12, 16 | cop 4376 |
. . 3
class
⟨((1^{st} ‘𝑥) ·_{N}
(1^{st} ‘𝑦)),
((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩ |
18 | 2, 3, 5, 5, 17 | cmpt2 6876 |
. 2
class (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |
19 | 1, 18 | wceq 1637 |
1
wff
·_{pQ} = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |