Detailed syntax breakdown of Definition df-rprm
Step | Hyp | Ref
| Expression |
1 | | crpm 19730 |
. 2
class
RPrime |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑤 |
6 | | cbs 16760 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6380 |
. . . 4
class
(Base‘𝑤) |
8 | | vp |
. . . . . . . . . . 11
setvar 𝑝 |
9 | 8 | cv 1542 |
. . . . . . . . . 10
class 𝑝 |
10 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
11 | 10 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
12 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
13 | 12 | cv 1542 |
. . . . . . . . . . 11
class 𝑦 |
14 | | cmulr 16803 |
. . . . . . . . . . . 12
class
.r |
15 | 5, 14 | cfv 6380 |
. . . . . . . . . . 11
class
(.r‘𝑤) |
16 | 11, 13, 15 | co 7213 |
. . . . . . . . . 10
class (𝑥(.r‘𝑤)𝑦) |
17 | | vd |
. . . . . . . . . . 11
setvar 𝑑 |
18 | 17 | cv 1542 |
. . . . . . . . . 10
class 𝑑 |
19 | 9, 16, 18 | wbr 5053 |
. . . . . . . . 9
wff 𝑝𝑑(𝑥(.r‘𝑤)𝑦) |
20 | 9, 11, 18 | wbr 5053 |
. . . . . . . . . 10
wff 𝑝𝑑𝑥 |
21 | 9, 13, 18 | wbr 5053 |
. . . . . . . . . 10
wff 𝑝𝑑𝑦 |
22 | 20, 21 | wo 847 |
. . . . . . . . 9
wff (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦) |
23 | 19, 22 | wi 4 |
. . . . . . . 8
wff (𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) |
24 | | cdsr 19656 |
. . . . . . . . 9
class
∥r |
25 | 5, 24 | cfv 6380 |
. . . . . . . 8
class
(∥r‘𝑤) |
26 | 23, 17, 25 | wsbc 3694 |
. . . . . . 7
wff
[(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) |
27 | 4 | cv 1542 |
. . . . . . 7
class 𝑏 |
28 | 26, 12, 27 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑏
[(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) |
29 | 28, 10, 27 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) |
30 | | cui 19657 |
. . . . . . . 8
class
Unit |
31 | 5, 30 | cfv 6380 |
. . . . . . 7
class
(Unit‘𝑤) |
32 | | c0g 16944 |
. . . . . . . . 9
class
0g |
33 | 5, 32 | cfv 6380 |
. . . . . . . 8
class
(0g‘𝑤) |
34 | 33 | csn 4541 |
. . . . . . 7
class
{(0g‘𝑤)} |
35 | 31, 34 | cun 3864 |
. . . . . 6
class
((Unit‘𝑤)
∪ {(0g‘𝑤)}) |
36 | 27, 35 | cdif 3863 |
. . . . 5
class (𝑏 ∖ ((Unit‘𝑤) ∪
{(0g‘𝑤)})) |
37 | 29, 8, 36 | crab 3065 |
. . . 4
class {𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))} |
38 | 4, 7, 37 | csb 3811 |
. . 3
class
⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))} |
39 | 2, 3, 38 | cmpt 5135 |
. 2
class (𝑤 ∈ V ↦
⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) |
40 | 1, 39 | wceq 1543 |
1
wff RPrime =
(𝑤 ∈ V ↦
⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑤) / 𝑑](𝑝𝑑(𝑥(.r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) |