Detailed syntax breakdown of Definition df-mri
Step | Hyp | Ref
| Expression |
1 | | cmri 16958 |
. 2
class
mrInd |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | cmre 16956 |
. . . . 5
class
Moore |
4 | 3 | crn 5526 |
. . . 4
class ran
Moore |
5 | 4 | cuni 4796 |
. . 3
class ∪ ran Moore |
6 | | vx |
. . . . . . . 8
setvar 𝑥 |
7 | 6 | cv 1541 |
. . . . . . 7
class 𝑥 |
8 | | vs |
. . . . . . . . . 10
setvar 𝑠 |
9 | 8 | cv 1541 |
. . . . . . . . 9
class 𝑠 |
10 | 7 | csn 4516 |
. . . . . . . . 9
class {𝑥} |
11 | 9, 10 | cdif 3840 |
. . . . . . . 8
class (𝑠 ∖ {𝑥}) |
12 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑐 |
13 | | cmrc 16957 |
. . . . . . . . 9
class
mrCls |
14 | 12, 13 | cfv 6339 |
. . . . . . . 8
class
(mrCls‘𝑐) |
15 | 11, 14 | cfv 6339 |
. . . . . . 7
class
((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) |
16 | 7, 15 | wcel 2114 |
. . . . . 6
wff 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) |
17 | 16 | wn 3 |
. . . . 5
wff ¬
𝑥 ∈
((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) |
18 | 17, 6, 9 | wral 3053 |
. . . 4
wff
∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) |
19 | 12 | cuni 4796 |
. . . . 5
class ∪ 𝑐 |
20 | 19 | cpw 4488 |
. . . 4
class 𝒫
∪ 𝑐 |
21 | 18, 8, 20 | crab 3057 |
. . 3
class {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))} |
22 | 2, 5, 21 | cmpt 5110 |
. 2
class (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}) |
23 | 1, 22 | wceq 1542 |
1
wff mrInd =
(𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}) |