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∈V→ACS⁡X∈Moore⁡𝒫X

Proof

Step Hyp Ref Expression
1 fveq2 ⊢x=X→ACS⁡x=ACS⁡X
2 pweq ⊢x=X→𝒫x=𝒫X
3 2 fveq2d ⊢x=X→Moore⁡𝒫x=Moore⁡𝒫X
4 1 3 eleq12d ⊢x=X→ACS⁡x∈Moore⁡𝒫x↔ACS⁡X∈Moore⁡𝒫X
5 acsmre ⊢a∈ACS⁡x→a∈Moore⁡x
6 mresspw ⊢a∈Moore⁡x→a⊆𝒫x
7 5 6 syl ⊢a∈ACS⁡x→a⊆𝒫x
8 5 7 elpwd ⊢a∈ACS⁡x→a∈𝒫𝒫x
9 8 ssriv ⊢ACS⁡x⊆𝒫𝒫x
10 9 a1i ⊢⊤→ACS⁡x⊆𝒫𝒫x
11 vex ⊢x∈V
12 mremre ⊢x∈V→Moore⁡x∈Moore⁡𝒫x
13 11 12 mp1i ⊢a⊆ACS⁡x→Moore⁡x∈Moore⁡𝒫x
14 5 ssriv ⊢ACS⁡x⊆Moore⁡x
15 sstr ⊢a⊆ACS⁡x∧ACS⁡x⊆Moore⁡x→a⊆Moore⁡x
16 14 15 mpan2 ⊢a⊆ACS⁡x→a⊆Moore⁡x
17 mrerintcl ⊢Moore⁡x∈Moore⁡𝒫x∧a⊆Moore⁡x→𝒫x∩⋂a∈Moore⁡x
18 13 16 17 syl2anc ⊢a⊆ACS⁡x→𝒫x∩⋂a∈Moore⁡x
19 ssel2 ⊢a⊆ACS⁡x∧d∈a→d∈ACS⁡x
20 19 acsmred ⊢a⊆ACS⁡x∧d∈a→d∈Moore⁡x
21 eqid ⊢mrCls⁡d=mrCls⁡d
22 20 21 mrcssvd ⊢a⊆ACS⁡x∧d∈a→mrCls⁡d⁡c⊆x
23 22 ralrimiva ⊢a⊆ACS⁡x→∀d∈amrCls⁡d⁡c⊆x
24 23 adantr ⊢a⊆ACS⁡x∧c∈𝒫x→∀d∈amrCls⁡d⁡c⊆x
25 iunss ⊢⋃d∈amrCls⁡d⁡c⊆x↔∀d∈amrCls⁡d⁡c⊆x
26 24 25 sylibr ⊢a⊆ACS⁡x∧c∈𝒫x→⋃d∈amrCls⁡d⁡c⊆x
27 11 elpw2 ⊢⋃d∈amrCls⁡d⁡c∈𝒫x↔⋃d∈amrCls⁡d⁡c⊆x
28 26 27 sylibr ⊢a⊆ACS⁡x∧c∈𝒫x→⋃d∈amrCls⁡d⁡c∈𝒫x
29 28 fmpttd ⊢a⊆ACS⁡x→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c:𝒫x⟶𝒫x
30 fssxp ⊢c∈𝒫x⟼⋃d∈amrCls⁡d⁡c:𝒫x⟶𝒫x→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c⊆𝒫x×𝒫x
31 29 30 syl ⊢a⊆ACS⁡x→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c⊆𝒫x×𝒫x
32 vpwex ⊢𝒫x∈V
33 32 32 xpex ⊢𝒫x×𝒫x∈V
34 ssexg ⊢c∈𝒫x⟼⋃d∈amrCls⁡d⁡c⊆𝒫x×𝒫x∧𝒫x×𝒫x∈V→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c∈V
35 31 33 34 sylancl ⊢a⊆ACS⁡x→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c∈V
36 19 adantlr ⊢a⊆ACS⁡x∧b∈𝒫x∧d∈a→d∈ACS⁡x
37 elpwi ⊢b∈𝒫x→b⊆x
38 37 ad2antlr ⊢a⊆ACS⁡x∧b∈𝒫x∧d∈a→b⊆x
39 21 acsfiel2 ⊢d∈ACS⁡x∧b⊆x→b∈d↔∀e∈𝒫b∩FinmrCls⁡d⁡e⊆b
40 36 38 39 syl2anc ⊢a⊆ACS⁡x∧b∈𝒫x∧d∈a→b∈d↔∀e∈𝒫b∩FinmrCls⁡d⁡e⊆b
41 40 ralbidva ⊢a⊆ACS⁡x∧b∈𝒫x→∀d∈ab∈d↔∀d∈a∀e∈𝒫b∩FinmrCls⁡d⁡e⊆b
42 iunss ⊢⋃d∈amrCls⁡d⁡e⊆b↔∀d∈amrCls⁡d⁡e⊆b
43 42 ralbii ⊢∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b↔∀e∈𝒫b∩Fin∀d∈amrCls⁡d⁡e⊆b
44 ralcom ⊢∀e∈𝒫b∩Fin∀d∈amrCls⁡d⁡e⊆b↔∀d∈a∀e∈𝒫b∩FinmrCls⁡d⁡e⊆b
45 43 44 bitri ⊢∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b↔∀d∈a∀e∈𝒫b∩FinmrCls⁡d⁡e⊆b
46 41 45 bitr4di ⊢a⊆ACS⁡x∧b∈𝒫x→∀d∈ab∈d↔∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b
47 elrint2 ⊢b∈𝒫x→b∈𝒫x∩⋂a↔∀d∈ab∈d
48 47 adantl ⊢a⊆ACS⁡x∧b∈𝒫x→b∈𝒫x∩⋂a↔∀d∈ab∈d
49 funmpt ⊢Fun⁡c∈𝒫x⟼⋃d∈amrCls⁡d⁡c
50 funiunfv ⊢Fun⁡c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→⋃e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e=⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin
51 49 50 ax-mp ⊢⋃e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e=⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin
52 51 sseq1i ⊢⋃e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
53 iunss ⊢⋃e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b↔∀e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b
54 eqid ⊢c∈𝒫x⟼⋃d∈amrCls⁡d⁡c=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c
55 fveq2 ⊢c=e→mrCls⁡d⁡c=mrCls⁡d⁡e
56 55 iuneq2d ⊢c=e→⋃d∈amrCls⁡d⁡c=⋃d∈amrCls⁡d⁡e
57 inss1 ⊢𝒫b∩Fin⊆𝒫b
58 37 sspwd ⊢b∈𝒫x→𝒫b⊆𝒫x
59 58 adantl ⊢a⊆ACS⁡x∧b∈𝒫x→𝒫b⊆𝒫x
60 57 59 sstrid ⊢a⊆ACS⁡x∧b∈𝒫x→𝒫b∩Fin⊆𝒫x
61 60 sselda ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→e∈𝒫x
62 20 21 mrcssvd ⊢a⊆ACS⁡x∧d∈a→mrCls⁡d⁡e⊆x
63 62 ralrimiva ⊢a⊆ACS⁡x→∀d∈amrCls⁡d⁡e⊆x
64 63 ad2antrr ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→∀d∈amrCls⁡d⁡e⊆x
65 iunss ⊢⋃d∈amrCls⁡d⁡e⊆x↔∀d∈amrCls⁡d⁡e⊆x
66 64 65 sylibr ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→⋃d∈amrCls⁡d⁡e⊆x
67 ssexg ⊢⋃d∈amrCls⁡d⁡e⊆x∧x∈V→⋃d∈amrCls⁡d⁡e∈V
68 66 11 67 sylancl ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→⋃d∈amrCls⁡d⁡e∈V
69 54 56 61 68 fvmptd3 ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e=⋃d∈amrCls⁡d⁡e
70 69 sseq1d ⊢a⊆ACS⁡x∧b∈𝒫x∧e∈𝒫b∩Fin→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b↔⋃d∈amrCls⁡d⁡e⊆b
71 70 ralbidva ⊢a⊆ACS⁡x∧b∈𝒫x→∀e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b↔∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b
72 53 71 bitrid ⊢a⊆ACS⁡x∧b∈𝒫x→⋃e∈𝒫b∩Finc∈𝒫x⟼⋃d∈amrCls⁡d⁡c⁡e⊆b↔∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b
73 52 72 bitr3id ⊢a⊆ACS⁡x∧b∈𝒫x→⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b↔∀e∈𝒫b∩Fin⋃d∈amrCls⁡d⁡e⊆b
74 46 48 73 3bitr4d ⊢a⊆ACS⁡x∧b∈𝒫x→b∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
75 74 ralrimiva ⊢a⊆ACS⁡x→∀b∈𝒫xb∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
76 29 75 jca ⊢a⊆ACS⁡x→c∈𝒫x⟼⋃d∈amrCls⁡d⁡c:𝒫x⟶𝒫x∧∀b∈𝒫xb∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
77 feq1 ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→f:𝒫x⟶𝒫x↔c∈𝒫x⟼⋃d∈amrCls⁡d⁡c:𝒫x⟶𝒫x
78 imaeq1 ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→f𝒫b∩Fin=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin
79 78 unieqd ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→⋃f𝒫b∩Fin=⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin
80 79 sseq1d ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→⋃f𝒫b∩Fin⊆b↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
81 80 bibi2d ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→b∈𝒫x∩⋂a↔⋃f𝒫b∩Fin⊆b↔b∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
82 81 ralbidv ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→∀b∈𝒫xb∈𝒫x∩⋂a↔⋃f𝒫b∩Fin⊆b↔∀b∈𝒫xb∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
83 77 82 anbi12d ⊢f=c∈𝒫x⟼⋃d∈amrCls⁡d⁡c→f:𝒫x⟶𝒫x∧∀b∈𝒫xb∈𝒫x∩⋂a↔⋃f𝒫b∩Fin⊆b↔c∈𝒫x⟼⋃d∈amrCls⁡d⁡c:𝒫x⟶𝒫x∧∀b∈𝒫xb∈𝒫x∩⋂a↔⋃c∈𝒫x⟼⋃d∈amrCls⁡d⁡c𝒫b∩Fin⊆b
84 35 76 83 spcedv ⊢a⊆ACS⁡x→∃ff:𝒫x⟶𝒫x∧∀b∈𝒫xb∈𝒫x∩⋂a↔⋃f𝒫b∩Fin⊆b
85 isacs ⊢𝒫x∩⋂a∈ACS⁡x↔𝒫x∩⋂a∈Moore⁡x∧∃ff:𝒫x⟶𝒫x∧∀b∈𝒫xb∈𝒫x∩⋂a↔⋃f𝒫b∩Fin⊆b
86 18 84 85 sylanbrc ⊢a⊆ACS⁡x→𝒫x∩⋂a∈ACS⁡x
87 86 adantl ⊢⊤∧a⊆ACS⁡x→𝒫x∩⋂a∈ACS⁡x
88 10 87 ismred2 ⊢⊤→ACS⁡x∈Moore⁡𝒫x
89 88 mptru ⊢ACS⁡x∈Moore⁡𝒫x
90 4 89 vtoclg ⊢X∈V→ACS⁡X∈Moore⁡𝒫X