This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( 𝑎 ⊆ ( 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 ‘ 𝒫 𝑋 ) )