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 ( 𝑋𝑉 → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )

Proof

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