Detailed syntax breakdown of Definition df-acs
| Step | Hyp | Ref
| Expression |
| 1 | | cacs 17628 |
. 2
class
ACS |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | 2 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 5 | 4 | cpw 4600 |
. . . . . . 7
class 𝒫
𝑥 |
| 6 | | vf |
. . . . . . . 8
setvar 𝑓 |
| 7 | 6 | cv 1539 |
. . . . . . 7
class 𝑓 |
| 8 | 5, 5, 7 | wf 6557 |
. . . . . 6
wff 𝑓:𝒫 𝑥⟶𝒫 𝑥 |
| 9 | | vs |
. . . . . . . . 9
setvar 𝑠 |
| 10 | | vc |
. . . . . . . . 9
setvar 𝑐 |
| 11 | 9, 10 | wel 2109 |
. . . . . . . 8
wff 𝑠 ∈ 𝑐 |
| 12 | 9 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑠 |
| 13 | 12 | cpw 4600 |
. . . . . . . . . . . 12
class 𝒫
𝑠 |
| 14 | | cfn 8985 |
. . . . . . . . . . . 12
class
Fin |
| 15 | 13, 14 | cin 3950 |
. . . . . . . . . . 11
class
(𝒫 𝑠 ∩
Fin) |
| 16 | 7, 15 | cima 5688 |
. . . . . . . . . 10
class (𝑓 “ (𝒫 𝑠 ∩ Fin)) |
| 17 | 16 | cuni 4907 |
. . . . . . . . 9
class ∪ (𝑓
“ (𝒫 𝑠 ∩
Fin)) |
| 18 | 17, 12 | wss 3951 |
. . . . . . . 8
wff ∪ (𝑓
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠 |
| 19 | 11, 18 | wb 206 |
. . . . . . 7
wff (𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) |
| 20 | 19, 9, 5 | wral 3061 |
. . . . . 6
wff
∀𝑠 ∈
𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) |
| 21 | 8, 20 | wa 395 |
. . . . 5
wff (𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) |
| 22 | 21, 6 | wex 1779 |
. . . 4
wff
∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) |
| 23 | | cmre 17625 |
. . . . 5
class
Moore |
| 24 | 4, 23 | cfv 6561 |
. . . 4
class
(Moore‘𝑥) |
| 25 | 22, 10, 24 | crab 3436 |
. . 3
class {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} |
| 26 | 2, 3, 25 | cmpt 5225 |
. 2
class (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) |
| 27 | 1, 26 | wceq 1540 |
1
wff ACS =
(𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) |