Detailed syntax breakdown of Definition df-nq
Step | Hyp | Ref
| Expression |
1 | | cnq 10609 |
. 2
class
Q |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
4 | | vy |
. . . . . . 7
setvar 𝑦 |
5 | 4 | cv 1541 |
. . . . . 6
class 𝑦 |
6 | | ceq 10608 |
. . . . . 6
class
~Q |
7 | 3, 5, 6 | wbr 5079 |
. . . . 5
wff 𝑥 ~Q
𝑦 |
8 | | c2nd 7823 |
. . . . . . . 8
class
2nd |
9 | 5, 8 | cfv 6432 |
. . . . . . 7
class
(2nd ‘𝑦) |
10 | 3, 8 | cfv 6432 |
. . . . . . 7
class
(2nd ‘𝑥) |
11 | | clti 10604 |
. . . . . . 7
class
<N |
12 | 9, 10, 11 | wbr 5079 |
. . . . . 6
wff
(2nd ‘𝑦) <N
(2nd ‘𝑥) |
13 | 12 | wn 3 |
. . . . 5
wff ¬
(2nd ‘𝑦)
<N (2nd ‘𝑥) |
14 | 7, 13 | wi 4 |
. . . 4
wff (𝑥 ~Q
𝑦 → ¬
(2nd ‘𝑦)
<N (2nd ‘𝑥)) |
15 | | cnpi 10601 |
. . . . 5
class
N |
16 | 15, 15 | cxp 5588 |
. . . 4
class
(N × N) |
17 | 14, 4, 16 | wral 3066 |
. . 3
wff
∀𝑦 ∈
(N × N)(𝑥 ~Q 𝑦 → ¬ (2nd
‘𝑦)
<N (2nd ‘𝑥)) |
18 | 17, 2, 16 | crab 3070 |
. 2
class {𝑥 ∈ (N ×
N) ∣ ∀𝑦 ∈ (N ×
N)(𝑥
~Q 𝑦 → ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥))} |
19 | 1, 18 | wceq 1542 |
1
wff
Q = {𝑥
∈ (N × N) ∣ ∀𝑦 ∈ (N ×
N)(𝑥
~Q 𝑦 → ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥))} |