Detailed syntax breakdown of Definition df-numer
Step | Hyp | Ref
| Expression |
1 | | cnumer 16418 |
. 2
class
numer |
2 | | vy |
. . 3
setvar 𝑦 |
3 | | cq 12670 |
. . 3
class
ℚ |
4 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
5 | 4 | cv 1540 |
. . . . . . . . 9
class 𝑥 |
6 | | c1st 7815 |
. . . . . . . . 9
class
1st |
7 | 5, 6 | cfv 6430 |
. . . . . . . 8
class
(1st ‘𝑥) |
8 | | c2nd 7816 |
. . . . . . . . 9
class
2nd |
9 | 5, 8 | cfv 6430 |
. . . . . . . 8
class
(2nd ‘𝑥) |
10 | | cgcd 16182 |
. . . . . . . 8
class
gcd |
11 | 7, 9, 10 | co 7268 |
. . . . . . 7
class
((1st ‘𝑥) gcd (2nd ‘𝑥)) |
12 | | c1 10856 |
. . . . . . 7
class
1 |
13 | 11, 12 | wceq 1541 |
. . . . . 6
wff
((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 |
14 | 2 | cv 1540 |
. . . . . . 7
class 𝑦 |
15 | | cdiv 11615 |
. . . . . . . 8
class
/ |
16 | 7, 9, 15 | co 7268 |
. . . . . . 7
class
((1st ‘𝑥) / (2nd ‘𝑥)) |
17 | 14, 16 | wceq 1541 |
. . . . . 6
wff 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)) |
18 | 13, 17 | wa 395 |
. . . . 5
wff
(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))) |
19 | | cz 12302 |
. . . . . 6
class
ℤ |
20 | | cn 11956 |
. . . . . 6
class
ℕ |
21 | 19, 20 | cxp 5586 |
. . . . 5
class (ℤ
× ℕ) |
22 | 18, 4, 21 | crio 7224 |
. . . 4
class
(℩𝑥
∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))) |
23 | 22, 6 | cfv 6430 |
. . 3
class
(1st ‘(℩𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))) |
24 | 2, 3, 23 | cmpt 5161 |
. 2
class (𝑦 ∈ ℚ ↦
(1st ‘(℩𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) |
25 | 1, 24 | wceq 1541 |
1
wff numer =
(𝑦 ∈ ℚ ↦
(1st ‘(℩𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) |