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 ∈ a mrCls ⁡ d ⁡ c ⊆ x
24 23 adantr ⊢ a ⊆ ACS ⁡ x ∧ c ∈ 𝒫 x → ∀ d ∈ a mrCls ⁡ d ⁡ c ⊆ x
25 iunss ⊢ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ x ↔ ∀ d ∈ a mrCls ⁡ d ⁡ c ⊆ x
26 24 25 sylibr ⊢ a ⊆ ACS ⁡ x ∧ c ∈ 𝒫 x → ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ x
27 11 elpw2 ⊢ ⋃ d ∈ a mrCls ⁡ d ⁡ c ∈ 𝒫 x ↔ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ x
28 26 27 sylibr ⊢ a ⊆ ACS ⁡ x ∧ c ∈ 𝒫 x → ⋃ d ∈ a mrCls ⁡ d ⁡ c ∈ 𝒫 x
29 28 fmpttd ⊢ a ⊆ ACS ⁡ x → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c : 𝒫 x ⟶ 𝒫 x
30 fssxp ⊢ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c : 𝒫 x ⟶ 𝒫 x → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ 𝒫 x × 𝒫 x
31 29 30 syl ⊢ a ⊆ ACS ⁡ x → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ 𝒫 x × 𝒫 x
32 vpwex ⊢ 𝒫 x ∈ V
33 32 32 xpex ⊢ 𝒫 x × 𝒫 x ∈ V
34 ssexg ⊢ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⊆ 𝒫 x × 𝒫 x ∧ 𝒫 x × 𝒫 x ∈ V → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ∈ V
35 31 33 34 sylancl ⊢ a ⊆ ACS ⁡ x → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ 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 ∩ Fin mrCls ⁡ d ⁡ e ⊆ b
40 36 38 39 syl2anc ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ d ∈ a → b ∈ d ↔ ∀ e ∈ 𝒫 b ∩ Fin mrCls ⁡ d ⁡ e ⊆ b
41 40 ralbidva ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → ∀ d ∈ a b ∈ d ↔ ∀ d ∈ a ∀ e ∈ 𝒫 b ∩ Fin mrCls ⁡ d ⁡ e ⊆ b
42 iunss ⊢ ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b ↔ ∀ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
43 42 ralbii ⊢ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b ↔ ∀ e ∈ 𝒫 b ∩ Fin ∀ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
44 ralcom ⊢ ∀ e ∈ 𝒫 b ∩ Fin ∀ d ∈ a mrCls ⁡ d ⁡ e ⊆ b ↔ ∀ d ∈ a ∀ e ∈ 𝒫 b ∩ Fin mrCls ⁡ d ⁡ e ⊆ b
45 43 44 bitri ⊢ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b ↔ ∀ d ∈ a ∀ e ∈ 𝒫 b ∩ Fin mrCls ⁡ d ⁡ e ⊆ b
46 41 45 bitr4di ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → ∀ d ∈ a b ∈ d ↔ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
47 elrint2 ⊢ b ∈ 𝒫 x → b ∈ 𝒫 x ∩ ⋂ a ↔ ∀ d ∈ a b ∈ d
48 47 adantl ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → b ∈ 𝒫 x ∩ ⋂ a ↔ ∀ d ∈ a b ∈ d
49 funmpt ⊢ Fun ⁡ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c
50 funiunfv ⊢ Fun ⁡ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → ⋃ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e = ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin
51 49 50 ax-mp ⊢ ⋃ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e = ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin
52 51 sseq1i ⊢ ⋃ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
53 iunss ⊢ ⋃ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b ↔ ∀ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b
54 eqid ⊢ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c
55 fveq2 ⊢ c = e → mrCls ⁡ d ⁡ c = mrCls ⁡ d ⁡ e
56 55 iuneq2d ⊢ c = e → ⋃ d ∈ a mrCls ⁡ d ⁡ c = ⋃ d ∈ a mrCls ⁡ 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 ∈ a mrCls ⁡ d ⁡ e ⊆ x
64 63 ad2antrr ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ e ∈ 𝒫 b ∩ Fin → ∀ d ∈ a mrCls ⁡ d ⁡ e ⊆ x
65 iunss ⊢ ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ x ↔ ∀ d ∈ a mrCls ⁡ d ⁡ e ⊆ x
66 64 65 sylibr ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ e ∈ 𝒫 b ∩ Fin → ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ x
67 ssexg ⊢ ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ x ∧ x ∈ V → ⋃ d ∈ a mrCls ⁡ d ⁡ e ∈ V
68 66 11 67 sylancl ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ e ∈ 𝒫 b ∩ Fin → ⋃ d ∈ a mrCls ⁡ d ⁡ e ∈ V
69 54 56 61 68 fvmptd3 ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ e ∈ 𝒫 b ∩ Fin → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e = ⋃ d ∈ a mrCls ⁡ d ⁡ e
70 69 sseq1d ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x ∧ e ∈ 𝒫 b ∩ Fin → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b ↔ ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
71 70 ralbidva ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → ∀ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b ↔ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
72 53 71 bitrid ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → ⋃ e ∈ 𝒫 b ∩ Fin c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c ⁡ e ⊆ b ↔ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
73 52 72 bitr3id ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b ↔ ∀ e ∈ 𝒫 b ∩ Fin ⋃ d ∈ a mrCls ⁡ d ⁡ e ⊆ b
74 46 48 73 3bitr4d ⊢ a ⊆ ACS ⁡ x ∧ b ∈ 𝒫 x → b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
75 74 ralrimiva ⊢ a ⊆ ACS ⁡ x → ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
76 29 75 jca ⊢ a ⊆ ACS ⁡ x → c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c : 𝒫 x ⟶ 𝒫 x ∧ ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
77 feq1 ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → f : 𝒫 x ⟶ 𝒫 x ↔ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c : 𝒫 x ⟶ 𝒫 x
78 imaeq1 ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → f 𝒫 b ∩ Fin = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin
79 78 unieqd ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → ⋃ f 𝒫 b ∩ Fin = ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin
80 79 sseq1d ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → ⋃ f 𝒫 b ∩ Fin ⊆ b ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
81 80 bibi2d ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ f 𝒫 b ∩ Fin ⊆ b ↔ b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
82 81 ralbidv ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ f 𝒫 b ∩ Fin ⊆ b ↔ ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
83 77 82 anbi12d ⊢ f = c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c → f : 𝒫 x ⟶ 𝒫 x ∧ ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ f 𝒫 b ∩ Fin ⊆ b ↔ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c : 𝒫 x ⟶ 𝒫 x ∧ ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ c ∈ 𝒫 x ⟼ ⋃ d ∈ a mrCls ⁡ d ⁡ c 𝒫 b ∩ Fin ⊆ b
84 35 76 83 spcedv ⊢ a ⊆ ACS ⁡ x → ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ b ∈ 𝒫 x b ∈ 𝒫 x ∩ ⋂ a ↔ ⋃ f 𝒫 b ∩ Fin ⊆ b
85 isacs ⊢ 𝒫 x ∩ ⋂ a ∈ ACS ⁡ x ↔ 𝒫 x ∩ ⋂ a ∈ Moore ⁡ x ∧ ∃ f f : 𝒫 x ⟶ 𝒫 x ∧ ∀ b ∈ 𝒫 x b ∈ 𝒫 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