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

Theorem mreacs 13576
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 5541 . . 3  |-  ( x  =  X  ->  (ACS `  x )  =  (ACS
`  X ) )
2 pweq 3641 . . . 4  |-  ( x  =  X  ->  ~P x  =  ~P X
)
32fveq2d 5545 . . 3  |-  ( x  =  X  ->  (Moore `  ~P x )  =  (Moore `  ~P X ) )
41, 3eleq12d 2364 . 2  |-  ( x  =  X  ->  (
(ACS `  x )  e.  (Moore `  ~P x
)  <->  (ACS `  X )  e.  (Moore `  ~P X ) ) )
5 acsmre 13570 . . . . . . . 8  |-  ( a  e.  (ACS `  x
)  ->  a  e.  (Moore `  x ) )
6 mresspw 13510 . . . . . . . 8  |-  ( a  e.  (Moore `  x
)  ->  a  C_  ~P x )
75, 6syl 15 . . . . . . 7  |-  ( a  e.  (ACS `  x
)  ->  a  C_  ~P x )
8 vex 2804 . . . . . . . 8  |-  a  e. 
_V
98elpw 3644 . . . . . . 7  |-  ( a  e.  ~P ~P x  <->  a 
C_  ~P x )
107, 9sylibr 203 . . . . . 6  |-  ( a  e.  (ACS `  x
)  ->  a  e.  ~P ~P x )
1110ssriv 3197 . . . . 5  |-  (ACS `  x )  C_  ~P ~P x
1211a1i 10 . . . 4  |-  (  T. 
->  (ACS `  x )  C_ 
~P ~P x )
13 vex 2804 . . . . . . . 8  |-  x  e. 
_V
14 mremre 13522 . . . . . . . 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 3197 . . . . . . . 8  |-  (ACS `  x )  C_  (Moore `  x )
17 sstr 3200 . . . . . . . 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 13515 . . . . . . 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 3188 . . . . . . . . . . . . . . . 16  |-  ( ( a  C_  (ACS `  x
)  /\  d  e.  a )  ->  d  e.  (ACS `  x )
)
22 acsmre 13570 . . . . . . . . . . . . . . . 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 2296 . . . . . . . . . . . . . . . 16  |-  (mrCls `  d )  =  (mrCls `  d )
2524mrcssv 13532 . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . 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 3959 . . . . . . . . . . . 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 4191 . . . . . . . . . . 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 2296 . . . . . . . . . 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 5700 . . . . . . . . 9  |-  ( a 
C_  (ACS `  x
)  ->  ( c  e.  ~P x  |->  U_ d  e.  a  ( (mrCls `  d ) `  c
) ) : ~P x
--> ~P x )
35 fssxp 5416 . . . . . . . . 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 4209 . . . . . . . . 9  |-  ~P x  e.  _V
3837, 37xpex 4817 . . . . . . . 8  |-  ( ~P x  X.  ~P x
)  e.  _V
39 ssexg 4176 . . . . . . . 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 3646 . . . . . . . . . . . . . 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 13573 . . . . . . . . . . . . 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 2572 . . . . . . . . . . 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 3959 . . . . . . . . . . . . 13  |-  ( U_ d  e.  a  (
(mrCls `  d ) `  e )  C_  b  <->  A. d  e.  a  ( (mrCls `  d ) `  e )  C_  b
)
4847ralbii 2580 . . . . . . . . . . . 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 2713 . . . . . . . . . . . 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 3920 . . . . . . . . . . 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 5306 . . . . . . . . . . . . 13  |-  Fun  (
c  e.  ~P x  |-> 
U_ d  e.  a  ( (mrCls `  d
) `  c )
)
55 funiunfv 5790 . . . . . . . . . . . . 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 3215 . . . . . . . . . . 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 3959 . . . . . . . . . . . 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 3402 . . . . . . . . . . . . . . . . 17  |-  ( ~P b  i^i  Fin )  C_ 
~P b
60 sspwb 4239 . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . 16  |-  ( ( a  C_  (ACS `  x
)  /\  b  e.  ~P x )  ->  ( ~P b  i^i  Fin )  C_ 
~P x )
6463sselda 3193 . . . . . . . . . . . . . . 15  |-  ( ( ( a  C_  (ACS `  x )  /\  b  e.  ~P x )  /\  e  e.  ( ~P b  i^i  Fin ) )  ->  e  e.  ~P x )
6524mrcssv 13532 . . . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . . 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 3959 . . . . . . . . . . . . . . . . 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 4176 . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . 17  |-  ( c  =  e  ->  (
(mrCls `  d ) `  c )  =  ( (mrCls `  d ) `  e ) )
7473iuneq2d 3946 . . . . . . . . . . . . . . . 16  |-  ( c  =  e  ->  U_ d  e.  a  ( (mrCls `  d ) `  c
)  =  U_ d  e.  a  ( (mrCls `  d ) `  e
) )
7574, 33fvmptg 5616 . . . . . . . . . . . . . . 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 3218 . . . . . . . . . . . . 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 2572 . . . . . . . . . . . 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 2639 . . . . . . . 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 5391 . . . . . . . . 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 5023 . . . . . . . . . . . . 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 3854 . . . . . . . . . . . 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 3218 . . . . . . . . . . 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 2576 . . . . . . . . 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 2882 . . . . . . 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 13569 . . . . . 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 13521 . . 3  |-  (  T. 
->  (ACS `  x )  e.  (Moore `  ~P x
) )
9796trud 1314 . 2  |-  (ACS `  x )  e.  (Moore `  ~P x )
984, 97vtoclg 2856 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 1531    = wceq 1632    e. wcel 1696   A.wral 2556   _Vcvv 2801    i^i cin 3164    C_ wss 3165   ~Pcpw 3638   U.cuni 3843   |^|cint 3878   U_ciun 3921    e. cmpt 4093    X. cxp 4703   "cima 4708   Fun wfun 5265   -->wf 5267   ` cfv 5271   Fincfn 6879  Moorecmre 13500  mrClscmrc 13501  ACScacs 13503
This theorem is referenced by:  acsfn1  13579  acsfn1c  13580  acsfn2  13581  submacs  14458  subgacs  14668  nsgacs  14669  lssacs  15740  acsfn1p  27610  subrgacs  27611  sdrgacs  27612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-mre 13504  df-mrc 13505  df-acs 13507
  Copyright terms: Public domain W3C validator