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 e. V -> ( ACS ` X ) e. ( Moore ` ~P X ) )

Proof

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