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 syl5bb
 |-  ( ( 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 ) )