Detailed syntax breakdown of Definition df-nacs
Step | Hyp | Ref
| Expression |
1 | | cnacs 40227 |
. 2
class
NoeACS |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vs |
. . . . . . . 8
setvar 𝑠 |
5 | 4 | cv 1542 |
. . . . . . 7
class 𝑠 |
6 | | vg |
. . . . . . . . 9
setvar 𝑔 |
7 | 6 | cv 1542 |
. . . . . . . 8
class 𝑔 |
8 | | vc |
. . . . . . . . . 10
setvar 𝑐 |
9 | 8 | cv 1542 |
. . . . . . . . 9
class 𝑐 |
10 | | cmrc 17086 |
. . . . . . . . 9
class
mrCls |
11 | 9, 10 | cfv 6380 |
. . . . . . . 8
class
(mrCls‘𝑐) |
12 | 7, 11 | cfv 6380 |
. . . . . . 7
class
((mrCls‘𝑐)‘𝑔) |
13 | 5, 12 | wceq 1543 |
. . . . . 6
wff 𝑠 = ((mrCls‘𝑐)‘𝑔) |
14 | 2 | cv 1542 |
. . . . . . . 8
class 𝑥 |
15 | 14 | cpw 4513 |
. . . . . . 7
class 𝒫
𝑥 |
16 | | cfn 8626 |
. . . . . . 7
class
Fin |
17 | 15, 16 | cin 3865 |
. . . . . 6
class
(𝒫 𝑥 ∩
Fin) |
18 | 13, 6, 17 | wrex 3062 |
. . . . 5
wff
∃𝑔 ∈
(𝒫 𝑥 ∩
Fin)𝑠 = ((mrCls‘𝑐)‘𝑔) |
19 | 18, 4, 9 | wral 3061 |
. . . 4
wff
∀𝑠 ∈
𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔) |
20 | | cacs 17088 |
. . . . 5
class
ACS |
21 | 14, 20 | cfv 6380 |
. . . 4
class
(ACS‘𝑥) |
22 | 19, 8, 21 | crab 3065 |
. . 3
class {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)} |
23 | 2, 3, 22 | cmpt 5135 |
. 2
class (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}) |
24 | 1, 23 | wceq 1543 |
1
wff NoeACS =
(𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)}) |