Detailed syntax breakdown of Definition df-ltpq
Step | Hyp | Ref
| Expression |
1 | | cltpq 7227 |
. 2
class
<pQ |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1347 |
. . . . . 6
class 𝑥 |
4 | | cnpi 7221 |
. . . . . . 7
class
N |
5 | 4, 4 | cxp 4607 |
. . . . . 6
class
(N × N) |
6 | 3, 5 | wcel 2141 |
. . . . 5
wff 𝑥 ∈ (N ×
N) |
7 | | vy |
. . . . . . 7
setvar 𝑦 |
8 | 7 | cv 1347 |
. . . . . 6
class 𝑦 |
9 | 8, 5 | wcel 2141 |
. . . . 5
wff 𝑦 ∈ (N ×
N) |
10 | 6, 9 | wa 103 |
. . . 4
wff (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) |
11 | | c1st 6114 |
. . . . . . 7
class
1st |
12 | 3, 11 | cfv 5196 |
. . . . . 6
class
(1st ‘𝑥) |
13 | | c2nd 6115 |
. . . . . . 7
class
2nd |
14 | 8, 13 | cfv 5196 |
. . . . . 6
class
(2nd ‘𝑦) |
15 | | cmi 7223 |
. . . . . 6
class
·N |
16 | 12, 14, 15 | co 5850 |
. . . . 5
class
((1st ‘𝑥) ·N
(2nd ‘𝑦)) |
17 | 8, 11 | cfv 5196 |
. . . . . 6
class
(1st ‘𝑦) |
18 | 3, 13 | cfv 5196 |
. . . . . 6
class
(2nd ‘𝑥) |
19 | 17, 18, 15 | co 5850 |
. . . . 5
class
((1st ‘𝑦) ·N
(2nd ‘𝑥)) |
20 | | clti 7224 |
. . . . 5
class
<N |
21 | 16, 19, 20 | wbr 3987 |
. . . 4
wff
((1st ‘𝑥) ·N
(2nd ‘𝑦))
<N ((1st ‘𝑦) ·N
(2nd ‘𝑥)) |
22 | 10, 21 | wa 103 |
. . 3
wff ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((1st
‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥))) |
23 | 22, 2, 7 | copab 4047 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((1st
‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)))} |
24 | 1, 23 | wceq 1348 |
1
wff
<pQ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((1st
‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)))} |