Detailed syntax breakdown of Definition df-rqp
Step | Hyp | Ref
| Expression |
1 | | crqp 33605 |
. 2
class
/Qp |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | cprime 16374 |
. . 3
class
ℙ |
4 | | ceqp 33604 |
. . . 4
class
~Qp |
5 | | vy |
. . . . 5
setvar 𝑦 |
6 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
7 | 6 | cv 1541 |
. . . . . . . . . 10
class 𝑓 |
8 | 7 | ccnv 5589 |
. . . . . . . . 9
class ◡𝑓 |
9 | | cz 12319 |
. . . . . . . . . 10
class
ℤ |
10 | | cc0 10872 |
. . . . . . . . . . 11
class
0 |
11 | 10 | csn 4567 |
. . . . . . . . . 10
class
{0} |
12 | 9, 11 | cdif 3889 |
. . . . . . . . 9
class (ℤ
∖ {0}) |
13 | 8, 12 | cima 5593 |
. . . . . . . 8
class (◡𝑓 “ (ℤ ∖
{0})) |
14 | | vx |
. . . . . . . . 9
setvar 𝑥 |
15 | 14 | cv 1541 |
. . . . . . . 8
class 𝑥 |
16 | 13, 15 | wss 3892 |
. . . . . . 7
wff (◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥 |
17 | | cuz 12581 |
. . . . . . . 8
class
ℤ≥ |
18 | 17 | crn 5591 |
. . . . . . 7
class ran
ℤ≥ |
19 | 16, 14, 18 | wrex 3067 |
. . . . . 6
wff
∃𝑥 ∈ ran
ℤ≥(◡𝑓 “ (ℤ ∖ {0}))
⊆ 𝑥 |
20 | | cmap 8598 |
. . . . . . 7
class
↑m |
21 | 9, 9, 20 | co 7271 |
. . . . . 6
class (ℤ
↑m ℤ) |
22 | 19, 6, 21 | crab 3070 |
. . . . 5
class {𝑓 ∈ (ℤ
↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} |
23 | 5 | cv 1541 |
. . . . . 6
class 𝑦 |
24 | 2 | cv 1541 |
. . . . . . . . . 10
class 𝑝 |
25 | | c1 10873 |
. . . . . . . . . 10
class
1 |
26 | | cmin 11205 |
. . . . . . . . . 10
class
− |
27 | 24, 25, 26 | co 7271 |
. . . . . . . . 9
class (𝑝 − 1) |
28 | | cfz 13238 |
. . . . . . . . 9
class
... |
29 | 10, 27, 28 | co 7271 |
. . . . . . . 8
class
(0...(𝑝 −
1)) |
30 | 9, 29, 20 | co 7271 |
. . . . . . 7
class (ℤ
↑m (0...(𝑝
− 1))) |
31 | 23, 30 | cin 3891 |
. . . . . 6
class (𝑦 ∩ (ℤ
↑m (0...(𝑝
− 1)))) |
32 | 23, 31 | cxp 5588 |
. . . . 5
class (𝑦 × (𝑦 ∩ (ℤ ↑m
(0...(𝑝 −
1))))) |
33 | 5, 22, 32 | csb 3837 |
. . . 4
class
⦋{𝑓
∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m
(0...(𝑝 −
1))))) |
34 | 4, 33 | cin 3891 |
. . 3
class (~Qp
∩ ⦋{𝑓
∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m
(0...(𝑝 −
1)))))) |
35 | 2, 3, 34 | cmpt 5162 |
. 2
class (𝑝 ∈ ℙ ↦ (~Qp
∩ ⦋{𝑓
∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m
(0...(𝑝 −
1))))))) |
36 | 1, 35 | wceq 1542 |
1
wff /Qp =
(𝑝 ∈ ℙ ↦
(~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ)
∣ ∃𝑥 ∈ ran
ℤ≥(◡𝑓 “ (ℤ ∖ {0}))
⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m
(0...(𝑝 −
1))))))) |