MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreacs Unicode version

Theorem mreacs 13560
Description: Algebraicity is a composible property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Assertion
Ref Expression
mreacs  |-  ( X  e.  V  ->  (ACS `  X )  e.  (Moore `  ~P X ) )

Proof of Theorem mreacs
Dummy variables  a 
b  c  x  d  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5525 . . 3  |-  ( x  =  X  ->  (ACS `  x )  =  (ACS
`  X ) )
2 pweq 3628 . . . 4  |-  ( x  =  X  ->  ~P x  =  ~P X
)
32fveq2d 5529 . . 3  |-  ( x  =  X  ->  (Moore `  ~P x )  =  (Moore `  ~P X ) )
41, 3eleq12d 2351 . 2  |-  ( x  =  X  ->  (
(ACS `  x )  e.  (Moore `  ~P x
)  <->  (ACS `  X )  e.  (Moore `  ~P X ) ) )
5 acsmre 13554 . . . . . . . 8  |-  ( a  e.  (ACS `  x
)  ->  a  e.  (Moore `  x ) )
6 mresspw 13494 . . . . . . . 8  |-  ( a  e.  (Moore `  x
)  ->  a  C_  ~P x )
75, 6syl 15 . . . . . . 7  |-  ( a  e.  (ACS `  x
)  ->  a  C_  ~P x )
8 vex 2791 . . . . . . . 8  |-  a  e. 
_V
98elpw 3631 . . . . . . 7  |-  ( a  e.  ~P ~P x  <->  a 
C_  ~P x )
107, 9sylibr 203 . . . . . 6  |-  ( a  e.  (ACS `  x
)  ->  a  e.  ~P ~P x )
1110ssriv 3184 . . . . 5  |-  (ACS `  x )  C_  ~P ~P x
1211a1i 10 . . . 4  |-  (  T. 
->  (ACS `  x )  C_ 
~P ~P x )
13 vex 2791 . . . . . . . 8  |-  x  e. 
_V
14 mremre 13506 . . . . . . . 8  |-  ( x  e.  _V  ->  (Moore `  x )  e.  (Moore `  ~P x ) )
1513, 14mp1i 11 . . . . . . 7  |-  ( a 
C_  (ACS `  x
)  ->  (Moore `  x
)  e.  (Moore `  ~P x ) )
165ssriv 3184 . . . . . . . 8  |-  (ACS `  x )  C_  (Moore `  x )
17 sstr 3187 . . . . . . . 8  |-  ( ( a  C_  (ACS `  x
)  /\  (ACS `  x
)  C_  (Moore `  x
) )  ->  a  C_  (Moore `  x )
)
1816, 17mpan2 652 . . . . . . 7  |-  ( a 
C_  (ACS `  x
)  ->  a  C_  (Moore `  x ) )
19 mrerintcl 13499 . . . . . . 7  |-  ( ( (Moore `  x )  e.  (Moore `  ~P x
)  /\  a  C_  (Moore `  x ) )  ->  ( ~P x  i^i  |^| a )  e.  (Moore `  x )
)
2015, 18, 19syl2anc 642 . . . . . 6  |-  ( a 
C_  (ACS `  x
)  ->  ( ~P x  i^i  |^| a )  e.  (Moore `  x )
)
21 ssel2 3175 . . . . . . . . . . . . . . . 16  |-  ( ( a  C_  (ACS `  x
)  /\  d  e.  a )  ->  d  e.  (ACS `  x )
)
22 acsmre 13554 . . . . . . . . . . . . . . . 16  |-  ( d  e.  (ACS `  x
)  ->  d  e.  (Moore `  x ) )
2321, 22syl 15 . . . . . . . . . . . . . . 15  |-  ( ( a  C_  (ACS `  x
)  /\  d  e.  a )  ->  d  e.  (Moore `  x )
)
24 eqid 2283 . . . . . . . . . . . . . . . 16  |-  (mrCls `  d )  =  (mrCls `  d )
2524mrcssv 13516 . . . . . . . . . . . . . . 15  |-  ( d  e.  (Moore `  x
)  ->  ( (mrCls `  d ) `  c
)  C_  x )
2623, 25syl 15 . . . . . . . . . . . . . 14  |-  ( ( a  C_  (ACS `  x
)  /\  d  e.  a )  ->  (
(mrCls `  d ) `  c )  C_  x
)
2726ralrimiva 2626 . . . . . . . . . . . . 13  |-  ( a 
C_  (ACS `  x
)  ->  A. d  e.  a  ( (mrCls `  d ) `  c
)  C_  x )
2827adantr 451 . . . . . . . . . . . 12  |-  ( ( a  C_  (ACS `  x
)  /\  c  e.  ~P x )  ->  A. d  e.  a  ( (mrCls `  d ) `  c
)  C_  x )
29 iunss 3943 . . . . . . . . . . . 12  |-  ( U_ d  e.  a  (
(mrCls `  d ) `  c )  C_  x  <->  A. d  e.  a  ( (mrCls `  d ) `  c )  C_  x
)
3028, 29sylibr 203 . . . . . . . . . . 11  |-  ( ( a  C_  (ACS `  x
)  /\  c  e.  ~P x )  ->  U_ d  e.  a  ( (mrCls `  d ) `  c
)  C_  x )
3113elpw2 4175 . . . . . . . . . . 11  |-  ( U_ d  e.  a  (
(mrCls `  d ) `  c )  e.  ~P x 
<-> 
U_ d  e.  a  ( (mrCls `  d
) `  c )  C_  x )
3230, 31sylibr 203 . . . . . . . . . 10  |-  ( ( a  C_  (ACS `  x
)  /\  c  e.  ~P x )  ->  U_ d  e.  a  ( (mrCls `  d ) `  c
)  e.  ~P x
)
33 eqid 2283 . . . . . . . . . 10  |-  ( c  e.  ~P x  |->  U_ d  e.  a  (
(mrCls `  d ) `  c ) )  =  ( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d
) `  c )
)
3432, 33fmptd 5684 . . . . . . . . 9  |-  ( a 
C_  (ACS `  x
)  ->  ( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d ) `  c
) ) : ~P x
--> ~P x )
35 fssxp 5400 . . . . . . . . 9  |-  ( ( 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 ) )
3634, 35syl 15 . . . . . . . 8  |-  ( a 
C_  (ACS `  x
)  ->  ( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d ) `  c
) )  C_  ( ~P x  X.  ~P x
) )
3713pwex 4193 . . . . . . . . 9  |-  ~P x  e.  _V
3837, 37xpex 4801 . . . . . . . 8  |-  ( ~P x  X.  ~P x
)  e.  _V
39 ssexg 4160 . . . . . . . 8  |-  ( ( ( 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 )
4036, 38, 39sylancl 643 . . . . . . 7  |-  ( a 
C_  (ACS `  x
)  ->  ( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d ) `  c
) )  e.  _V )
4121adantlr 695 . . . . . . . . . . . . 13  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  d  e.  a )  ->  d  e.  (ACS `  x ) )
42 elpwi 3633 . . . . . . . . . . . . . 14  |-  ( b  e.  ~P x  -> 
b  C_  x )
4342ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  d  e.  a )  ->  b  C_  x )
4424acsfiel2 13557 . . . . . . . . . . . . 13  |-  ( ( d  e.  (ACS `  x )  /\  b  C_  x )  ->  (
b  e.  d  <->  A. e  e.  ( ~P b  i^i 
Fin ) ( (mrCls `  d ) `  e
)  C_  b )
)
4541, 43, 44syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
4645ralbidva 2559 . . . . . . . . . . 11  |-  ( ( 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 )
)
47 iunss 3943 . . . . . . . . . . . . 13  |-  ( U_ d  e.  a  (
(mrCls `  d ) `  e )  C_  b  <->  A. d  e.  a  ( (mrCls `  d ) `  e )  C_  b
)
4847ralbii 2567 . . . . . . . . . . . 12  |-  ( 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 )
49 ralcom 2700 . . . . . . . . . . . 12  |-  ( 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
)
5048, 49bitri 240 . . . . . . . . . . 11  |-  ( 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
)
5146, 50syl6bbr 254 . . . . . . . . . 10  |-  ( ( 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 )
)
52 elrint2 3904 . . . . . . . . . . 11  |-  ( b  e.  ~P x  -> 
( b  e.  ( ~P x  i^i  |^| a )  <->  A. d  e.  a  b  e.  d ) )
5352adantl 452 . . . . . . . . . 10  |-  ( ( a  C_  (ACS `  x
)  /\  b  e.  ~P x )  ->  (
b  e.  ( ~P x  i^i  |^| a
)  <->  A. d  e.  a  b  e.  d ) )
54 funmpt 5290 . . . . . . . . . . . . 13  |-  Fun  (
c  e.  ~P x  |-> 
U_ d  e.  a  ( (mrCls `  d
) `  c )
)
55 funiunfv 5774 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
5654, 55ax-mp 8 . . . . . . . . . . . 12  |-  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 ) )
5756sseq1i 3202 . . . . . . . . . . 11  |-  ( 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 )
58 iunss 3943 . . . . . . . . . . . 12  |-  ( 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
)
59 inss1 3389 . . . . . . . . . . . . . . . . 17  |-  ( ~P b  i^i  Fin )  C_ 
~P b
60 sspwb 4223 . . . . . . . . . . . . . . . . . . 19  |-  ( b 
C_  x  <->  ~P b  C_ 
~P x )
6142, 60sylib 188 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ~P x  ->  ~P b  C_  ~P x
)
6261adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( a  C_  (ACS `  x
)  /\  b  e.  ~P x )  ->  ~P b  C_  ~P x )
6359, 62syl5ss 3190 . . . . . . . . . . . . . . . 16  |-  ( ( a  C_  (ACS `  x
)  /\  b  e.  ~P x )  ->  ( ~P b  i^i  Fin )  C_ 
~P x )
6463sselda 3180 . . . . . . . . . . . . . . 15  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  e  e.  ( ~P b  i^i  Fin ) )  ->  e  e.  ~P x )
6524mrcssv 13516 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  (Moore `  x
)  ->  ( (mrCls `  d ) `  e
)  C_  x )
6623, 65syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  C_  (ACS `  x
)  /\  d  e.  a )  ->  (
(mrCls `  d ) `  e )  C_  x
)
6766ralrimiva 2626 . . . . . . . . . . . . . . . . . 18  |-  ( a 
C_  (ACS `  x
)  ->  A. d  e.  a  ( (mrCls `  d ) `  e
)  C_  x )
6867ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  e  e.  ( ~P b  i^i  Fin ) )  ->  A. d  e.  a  ( (mrCls `  d
) `  e )  C_  x )
69 iunss 3943 . . . . . . . . . . . . . . . . 17  |-  ( U_ d  e.  a  (
(mrCls `  d ) `  e )  C_  x  <->  A. d  e.  a  ( (mrCls `  d ) `  e )  C_  x
)
7068, 69sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  e  e.  ( ~P b  i^i  Fin ) )  ->  U_ d  e.  a  ( (mrCls `  d
) `  e )  C_  x )
71 ssexg 4160 . . . . . . . . . . . . . . . 16  |-  ( (
U_ d  e.  a  ( (mrCls `  d
) `  e )  C_  x  /\  x  e. 
_V )  ->  U_ d  e.  a  ( (mrCls `  d ) `  e
)  e.  _V )
7270, 13, 71sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  e  e.  ( ~P b  i^i  Fin ) )  ->  U_ d  e.  a  ( (mrCls `  d
) `  e )  e.  _V )
73 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( c  =  e  ->  (
(mrCls `  d ) `  c )  =  ( (mrCls `  d ) `  e ) )
7473iuneq2d 3930 . . . . . . . . . . . . . . . 16  |-  ( c  =  e  ->  U_ d  e.  a  ( (mrCls `  d ) `  c
)  =  U_ d  e.  a  ( (mrCls `  d ) `  e
) )
7574, 33fvmptg 5600 . . . . . . . . . . . . . . 15  |-  ( ( e  e.  ~P x  /\  U_ d  e.  a  ( (mrCls `  d
) `  e )  e.  _V )  ->  (
( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d
) `  c )
) `  e )  =  U_ d  e.  a  ( (mrCls `  d
) `  e )
)
7664, 72, 75syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
7776sseq1d 3205 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
7877ralbidva 2559 . . . . . . . . . . . 12  |-  ( ( 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 )
)
7958, 78syl5bb 248 . . . . . . . . . . 11  |-  ( ( 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 )
)
8057, 79syl5bbr 250 . . . . . . . . . 10  |-  ( ( 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 )
)
8151, 53, 803bitr4d 276 . . . . . . . . 9  |-  ( ( 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 ) )
8281ralrimiva 2626 . . . . . . . 8  |-  ( 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 )
)
8334, 82jca 518 . . . . . . 7  |-  ( 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 )
) )
84 feq1 5375 . . . . . . . . 9  |-  ( 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 ) )
85 imaeq1 5007 . . . . . . . . . . . . 13  |-  ( 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 )
) )
8685unieqd 3838 . . . . . . . . . . . 12  |-  ( 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 )
) )
8786sseq1d 3205 . . . . . . . . . . 11  |-  ( 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 )
)
8887bibi2d 309 . . . . . . . . . 10  |-  ( 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 ) ) )
8988ralbidv 2563 . . . . . . . . 9  |-  ( 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 )
) )
9084, 89anbi12d 691 . . . . . . . 8  |-  ( 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 )
) ) )
9190spcegv 2869 . . . . . . 7  |-  ( ( c  e.  ~P x  |-> 
U_ d  e.  a  ( (mrCls `  d
) `  c )
)  e.  _V  ->  ( ( ( 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 )
)  ->  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 )
) ) )
9240, 83, 91sylc 56 . . . . . 6  |-  ( 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 )
) )
93 isacs 13553 . . . . . 6  |-  ( ( ~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 )
) ) )
9420, 92, 93sylanbrc 645 . . . . 5  |-  ( a 
C_  (ACS `  x
)  ->  ( ~P x  i^i  |^| a )  e.  (ACS `  x )
)
9594adantl 452 . . . 4  |-  ( (  T.  /\  a  C_  (ACS `  x ) )  ->  ( ~P x  i^i  |^| a )  e.  (ACS `  x )
)
9612, 95ismred2 13505 . . 3  |-  (  T. 
->  (ACS `  x )  e.  (Moore `  ~P x
) )
9796trud 1314 . 2  |-  (ACS `  x )  e.  (Moore `  ~P x )
984, 97vtoclg 2843 1  |-  ( X  e.  V  ->  (ACS `  X )  e.  (Moore `  ~P X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    T. wtru 1307   E.wex 1528    = wceq 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788    i^i cin 3151    C_ wss 3152   ~Pcpw 3625   U.cuni 3827   |^|cint 3862   U_ciun 3905    e. cmpt 4077    X. cxp 4687   "cima 4692   Fun wfun 5249   -->wf 5251   ` cfv 5255   Fincfn 6863  Moorecmre 13484  mrClscmrc 13485  ACScacs 13487
This theorem is referenced by:  acsfn1  13563  acsfn1c  13564  acsfn2  13565  submacs  14442  subgacs  14652  nsgacs  14653  lssacs  15724  acsfn1p  26919  subrgacs  26920  sdrgacs  26921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-mre 13488  df-mrc 13489  df-acs 13491
  Copyright terms: Public domain W3C validator