# Metamath Proof Explorer

## Theorem mreacs

Description: Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion mreacs ${⊢}{X}\in {V}\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{x}={X}\to \mathrm{ACS}\left({x}\right)=\mathrm{ACS}\left({X}\right)$
2 pweq ${⊢}{x}={X}\to 𝒫{x}=𝒫{X}$
3 2 fveq2d ${⊢}{x}={X}\to \mathrm{Moore}\left(𝒫{x}\right)=\mathrm{Moore}\left(𝒫{X}\right)$
4 1 3 eleq12d ${⊢}{x}={X}\to \left(\mathrm{ACS}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)↔\mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)\right)$
5 acsmre ${⊢}{a}\in \mathrm{ACS}\left({x}\right)\to {a}\in \mathrm{Moore}\left({x}\right)$
6 mresspw ${⊢}{a}\in \mathrm{Moore}\left({x}\right)\to {a}\subseteq 𝒫{x}$
7 5 6 syl ${⊢}{a}\in \mathrm{ACS}\left({x}\right)\to {a}\subseteq 𝒫{x}$
8 5 7 elpwd ${⊢}{a}\in \mathrm{ACS}\left({x}\right)\to {a}\in 𝒫𝒫{x}$
9 8 ssriv ${⊢}\mathrm{ACS}\left({x}\right)\subseteq 𝒫𝒫{x}$
10 9 a1i ${⊢}\top \to \mathrm{ACS}\left({x}\right)\subseteq 𝒫𝒫{x}$
11 vex ${⊢}{x}\in \mathrm{V}$
12 mremre ${⊢}{x}\in \mathrm{V}\to \mathrm{Moore}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)$
13 11 12 mp1i ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \mathrm{Moore}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)$
14 5 ssriv ${⊢}\mathrm{ACS}\left({x}\right)\subseteq \mathrm{Moore}\left({x}\right)$
15 sstr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge \mathrm{ACS}\left({x}\right)\subseteq \mathrm{Moore}\left({x}\right)\right)\to {a}\subseteq \mathrm{Moore}\left({x}\right)$
16 14 15 mpan2 ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to {a}\subseteq \mathrm{Moore}\left({x}\right)$
17 mrerintcl ${⊢}\left(\mathrm{Moore}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)\wedge {a}\subseteq \mathrm{Moore}\left({x}\right)\right)\to 𝒫{x}\cap \bigcap {a}\in \mathrm{Moore}\left({x}\right)$
18 13 16 17 syl2anc ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to 𝒫{x}\cap \bigcap {a}\in \mathrm{Moore}\left({x}\right)$
19 ssel2 ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {d}\in {a}\right)\to {d}\in \mathrm{ACS}\left({x}\right)$
20 19 acsmred ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {d}\in {a}\right)\to {d}\in \mathrm{Moore}\left({x}\right)$
21 eqid ${⊢}\mathrm{mrCls}\left({d}\right)=\mathrm{mrCls}\left({d}\right)$
22 20 21 mrcssvd ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {d}\in {a}\right)\to \mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
23 22 ralrimiva ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
24 23 adantr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {c}\in 𝒫{x}\right)\to \forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
25 iunss ${⊢}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
26 24 25 sylibr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {c}\in 𝒫{x}\right)\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
27 11 elpw2 ${⊢}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\in 𝒫{x}↔\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\subseteq {x}$
28 26 27 sylibr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {c}\in 𝒫{x}\right)\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\in 𝒫{x}$
29 28 fmpttd ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right):𝒫{x}⟶𝒫{x}$
30 fssxp ${⊢}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right):𝒫{x}⟶𝒫{x}\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\subseteq 𝒫{x}×𝒫{x}$
31 29 30 syl ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\subseteq 𝒫{x}×𝒫{x}$
32 vpwex ${⊢}𝒫{x}\in \mathrm{V}$
33 32 32 xpex ${⊢}𝒫{x}×𝒫{x}\in \mathrm{V}$
34 ssexg ${⊢}\left(\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\subseteq 𝒫{x}×𝒫{x}\wedge 𝒫{x}×𝒫{x}\in \mathrm{V}\right)\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\in \mathrm{V}$
35 31 33 34 sylancl ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\in \mathrm{V}$
36 19 adantlr ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {d}\in {a}\right)\to {d}\in \mathrm{ACS}\left({x}\right)$
37 elpwi ${⊢}{b}\in 𝒫{x}\to {b}\subseteq {x}$
38 37 ad2antlr ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {d}\in {a}\right)\to {b}\subseteq {x}$
39 21 acsfiel2 ${⊢}\left({d}\in \mathrm{ACS}\left({x}\right)\wedge {b}\subseteq {x}\right)\to \left({b}\in {d}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
40 36 38 39 syl2anc ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {d}\in {a}\right)\to \left({b}\in {d}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
41 40 ralbidva ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left(\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}{b}\in {d}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
42 iunss ${⊢}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}$
43 42 ralbii ${⊢}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}$
44 ralcom ${⊢}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}$
45 43 44 bitri ${⊢}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}$
46 41 45 syl6bbr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left(\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}{b}\in {d}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
47 elrint2 ${⊢}{b}\in 𝒫{x}\to \left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}{b}\in {d}\right)$
48 47 adantl ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}{b}\in {d}\right)$
49 funmpt ${⊢}\mathrm{Fun}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)$
50 funiunfv ${⊢}\mathrm{Fun}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \bigcup _{{e}\in 𝒫{b}\cap \mathrm{Fin}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)=\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]$
51 49 50 ax-mp ${⊢}\bigcup _{{e}\in 𝒫{b}\cap \mathrm{Fin}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)=\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]$
52 51 sseq1i ${⊢}\bigcup _{{e}\in 𝒫{b}\cap \mathrm{Fin}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}$
53 iunss ${⊢}\bigcup _{{e}\in 𝒫{b}\cap \mathrm{Fin}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}$
54 eqid ${⊢}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)$
55 fveq2 ${⊢}{c}={e}\to \mathrm{mrCls}\left({d}\right)\left({c}\right)=\mathrm{mrCls}\left({d}\right)\left({e}\right)$
56 55 iuneq2d ${⊢}{c}={e}\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)=\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)$
57 inss1 ${⊢}𝒫{b}\cap \mathrm{Fin}\subseteq 𝒫{b}$
58 sspwb ${⊢}{b}\subseteq {x}↔𝒫{b}\subseteq 𝒫{x}$
59 37 58 sylib ${⊢}{b}\in 𝒫{x}\to 𝒫{b}\subseteq 𝒫{x}$
60 59 adantl ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to 𝒫{b}\subseteq 𝒫{x}$
61 57 60 sstrid ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to 𝒫{b}\cap \mathrm{Fin}\subseteq 𝒫{x}$
62 61 sselda ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to {e}\in 𝒫{x}$
63 20 21 mrcssvd ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {d}\in {a}\right)\to \mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}$
64 63 ralrimiva ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}$
65 64 ad2antrr ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to \forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}$
66 iunss ${⊢}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}↔\forall {d}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}$
67 65 66 sylibr ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}$
68 ssexg ${⊢}\left(\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {x}\wedge {x}\in \mathrm{V}\right)\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\in \mathrm{V}$
69 67 11 68 sylancl ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to \bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\in \mathrm{V}$
70 54 56 62 69 fvmptd3 ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)=\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)$
71 70 sseq1d ${⊢}\left(\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\wedge {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\right)\to \left(\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}↔\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
72 71 ralbidva ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left(\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
73 53 72 syl5bb ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left(\bigcup _{{e}\in 𝒫{b}\cap \mathrm{Fin}}\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left({e}\right)\subseteq {b}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
74 52 73 syl5bbr ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left(\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}↔\forall {e}\in \left(𝒫{b}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({e}\right)\subseteq {b}\right)$
75 46 48 74 3bitr4d ${⊢}\left({a}\subseteq \mathrm{ACS}\left({x}\right)\wedge {b}\in 𝒫{x}\right)\to \left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)$
76 75 ralrimiva ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)$
77 29 76 jca ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \left(\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right):𝒫{x}⟶𝒫{x}\wedge \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)$
78 feq1 ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \left({f}:𝒫{x}⟶𝒫{x}↔\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right):𝒫{x}⟶𝒫{x}\right)$
79 imaeq1 ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to {f}\left[𝒫{b}\cap \mathrm{Fin}\right]=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]$
80 79 unieqd ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]=\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]$
81 80 sseq1d ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \left(\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)$
82 81 bibi2d ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \left(\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)↔\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)$
83 82 ralbidv ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \left(\forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)↔\forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)$
84 78 83 anbi12d ${⊢}{f}=\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\to \left(\left({f}:𝒫{x}⟶𝒫{x}\wedge \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)↔\left(\left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right):𝒫{x}⟶𝒫{x}\wedge \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup \left({c}\in 𝒫{x}⟼\bigcup _{{d}\in {a}}\mathrm{mrCls}\left({d}\right)\left({c}\right)\right)\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)\right)$
85 35 77 84 spcedv ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:𝒫{x}⟶𝒫{x}\wedge \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)$
86 isacs ${⊢}𝒫{x}\cap \bigcap {a}\in \mathrm{ACS}\left({x}\right)↔\left(𝒫{x}\cap \bigcap {a}\in \mathrm{Moore}\left({x}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:𝒫{x}⟶𝒫{x}\wedge \forall {b}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left({b}\in \left(𝒫{x}\cap \bigcap {a}\right)↔\bigcup {f}\left[𝒫{b}\cap \mathrm{Fin}\right]\subseteq {b}\right)\right)\right)$
87 18 85 86 sylanbrc ${⊢}{a}\subseteq \mathrm{ACS}\left({x}\right)\to 𝒫{x}\cap \bigcap {a}\in \mathrm{ACS}\left({x}\right)$
88 87 adantl ${⊢}\left(\top \wedge {a}\subseteq \mathrm{ACS}\left({x}\right)\right)\to 𝒫{x}\cap \bigcap {a}\in \mathrm{ACS}\left({x}\right)$
89 10 88 ismred2 ${⊢}\top \to \mathrm{ACS}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)$
90 89 mptru ${⊢}\mathrm{ACS}\left({x}\right)\in \mathrm{Moore}\left(𝒫{x}\right)$
91 4 90 vtoclg ${⊢}{X}\in {V}\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$