Detailed syntax breakdown of Definition df-domn
Step | Hyp | Ref
| Expression |
1 | | cdomn 20558 |
. 2
class
Domn |
2 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
3 | 2 | cv 1537 |
. . . . . . . . . 10
class 𝑥 |
4 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
5 | 4 | cv 1537 |
. . . . . . . . . 10
class 𝑦 |
6 | | vr |
. . . . . . . . . . . 12
setvar 𝑟 |
7 | 6 | cv 1537 |
. . . . . . . . . . 11
class 𝑟 |
8 | | cmulr 16970 |
. . . . . . . . . . 11
class
.r |
9 | 7, 8 | cfv 6435 |
. . . . . . . . . 10
class
(.r‘𝑟) |
10 | 3, 5, 9 | co 7282 |
. . . . . . . . 9
class (𝑥(.r‘𝑟)𝑦) |
11 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
12 | 11 | cv 1537 |
. . . . . . . . 9
class 𝑧 |
13 | 10, 12 | wceq 1538 |
. . . . . . . 8
wff (𝑥(.r‘𝑟)𝑦) = 𝑧 |
14 | 2, 11 | weq 1963 |
. . . . . . . . 9
wff 𝑥 = 𝑧 |
15 | 4, 11 | weq 1963 |
. . . . . . . . 9
wff 𝑦 = 𝑧 |
16 | 14, 15 | wo 844 |
. . . . . . . 8
wff (𝑥 = 𝑧 ∨ 𝑦 = 𝑧) |
17 | 13, 16 | wi 4 |
. . . . . . 7
wff ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
18 | | vb |
. . . . . . . 8
setvar 𝑏 |
19 | 18 | cv 1537 |
. . . . . . 7
class 𝑏 |
20 | 17, 4, 19 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
21 | 20, 2, 19 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
22 | | c0g 17157 |
. . . . . 6
class
0g |
23 | 7, 22 | cfv 6435 |
. . . . 5
class
(0g‘𝑟) |
24 | 21, 11, 23 | wsbc 3715 |
. . . 4
wff
[(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
25 | | cbs 16919 |
. . . . 5
class
Base |
26 | 7, 25 | cfv 6435 |
. . . 4
class
(Base‘𝑟) |
27 | 24, 18, 26 | wsbc 3715 |
. . 3
wff
[(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
28 | | cnzr 20535 |
. . 3
class
NzRing |
29 | 27, 6, 28 | crab 3136 |
. 2
class {𝑟 ∈ NzRing ∣
[(Base‘𝑟) /
𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} |
30 | 1, 29 | wceq 1538 |
1
wff Domn =
{𝑟 ∈ NzRing ∣
[(Base‘𝑟) /
𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} |