| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfvex 6944 | . 2
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝑋 ∈ V) | 
| 2 |  | elfvex 6944 | . . 3
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ V) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))) → 𝑋 ∈ V) | 
| 4 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑋 → (Moore‘𝑥) = (Moore‘𝑋)) | 
| 5 |  | pweq 4614 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋) | 
| 6 | 5, 5 | feq23d 6731 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ 𝑓:𝒫 𝑋⟶𝒫 𝑋)) | 
| 7 | 5 | raleqdv 3326 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))) | 
| 8 | 6, 7 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | 
| 9 | 8 | exbidv 1921 | . . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | 
| 10 | 4, 9 | rabeqbidv 3455 | . . . . 5
⊢ (𝑥 = 𝑋 → {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} = {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) | 
| 11 |  | df-acs 17632 | . . . . 5
⊢ ACS =
(𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) | 
| 12 |  | fvex 6919 | . . . . . 6
⊢
(Moore‘𝑋)
∈ V | 
| 13 | 12 | rabex 5339 | . . . . 5
⊢ {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} ∈ V | 
| 14 | 10, 11, 13 | fvmpt 7016 | . . . 4
⊢ (𝑋 ∈ V →
(ACS‘𝑋) = {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) | 
| 15 | 14 | eleq2d 2827 | . . 3
⊢ (𝑋 ∈ V → (𝐶 ∈ (ACS‘𝑋) ↔ 𝐶 ∈ {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})) | 
| 16 |  | eleq2 2830 | . . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑠 ∈ 𝑐 ↔ 𝑠 ∈ 𝐶)) | 
| 17 | 16 | bibi1d 343 | . . . . . . 7
⊢ (𝑐 = 𝐶 → ((𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ (𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))) | 
| 18 | 17 | ralbidv 3178 | . . . . . 6
⊢ (𝑐 = 𝐶 → (∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))) | 
| 19 | 18 | anbi2d 630 | . . . . 5
⊢ (𝑐 = 𝐶 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | 
| 20 | 19 | exbidv 1921 | . . . 4
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | 
| 21 | 20 | elrab 3692 | . . 3
⊢ (𝐶 ∈ {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | 
| 22 | 15, 21 | bitrdi 287 | . 2
⊢ (𝑋 ∈ V → (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))) | 
| 23 | 1, 3, 22 | pm5.21nii 378 | 1
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) |