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

Theorem mreacs 13562
 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 ACS Moore

Proof of Theorem mreacs
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5527 . . 3 ACS ACS
2 pweq 3630 . . . 4
32fveq2d 5531 . . 3 Moore Moore
41, 3eleq12d 2353 . 2 ACS Moore ACS Moore
5 acsmre 13556 . . . . . . . 8 ACS Moore
6 mresspw 13496 . . . . . . . 8 Moore
75, 6syl 15 . . . . . . 7 ACS
8 vex 2793 . . . . . . . 8
98elpw 3633 . . . . . . 7
107, 9sylibr 203 . . . . . 6 ACS
1110ssriv 3186 . . . . 5 ACS
1211a1i 10 . . . 4 ACS
13 vex 2793 . . . . . . . 8
14 mremre 13508 . . . . . . . 8 Moore Moore
1513, 14mp1i 11 . . . . . . 7 ACS Moore Moore
165ssriv 3186 . . . . . . . 8 ACS Moore
17 sstr 3189 . . . . . . . 8 ACS ACS Moore Moore
1816, 17mpan2 652 . . . . . . 7 ACS Moore
19 mrerintcl 13501 . . . . . . 7 Moore Moore Moore Moore
2015, 18, 19syl2anc 642 . . . . . 6 ACS Moore
21 ssel2 3177 . . . . . . . . . . . . . . . 16 ACS ACS
22 acsmre 13556 . . . . . . . . . . . . . . . 16 ACS Moore
2321, 22syl 15 . . . . . . . . . . . . . . 15 ACS Moore
24 eqid 2285 . . . . . . . . . . . . . . . 16 mrCls mrCls
2524mrcssv 13518 . . . . . . . . . . . . . . 15 Moore mrCls
2623, 25syl 15 . . . . . . . . . . . . . 14 ACS mrCls
2726ralrimiva 2628 . . . . . . . . . . . . 13 ACS mrCls
2827adantr 451 . . . . . . . . . . . 12 ACS mrCls
29 iunss 3945 . . . . . . . . . . . 12 mrCls mrCls
3028, 29sylibr 203 . . . . . . . . . . 11 ACS mrCls
3113elpw2 4177 . . . . . . . . . . 11 mrCls mrCls
3230, 31sylibr 203 . . . . . . . . . 10 ACS mrCls
33 eqid 2285 . . . . . . . . . 10 mrCls mrCls
3432, 33fmptd 5686 . . . . . . . . 9 ACS mrCls
35 fssxp 5402 . . . . . . . . 9 mrCls mrCls
3634, 35syl 15 . . . . . . . 8 ACS mrCls
3713pwex 4195 . . . . . . . . 9
3837, 37xpex 4803 . . . . . . . 8
39 ssexg 4162 . . . . . . . 8 mrCls mrCls
4036, 38, 39sylancl 643 . . . . . . 7 ACS mrCls
4121adantlr 695 . . . . . . . . . . . . 13 ACS ACS
42 elpwi 3635 . . . . . . . . . . . . . 14
4342ad2antlr 707 . . . . . . . . . . . . 13 ACS
4424acsfiel2 13559 . . . . . . . . . . . . 13 ACS mrCls
4541, 43, 44syl2anc 642 . . . . . . . . . . . 12 ACS mrCls
4645ralbidva 2561 . . . . . . . . . . 11 ACS mrCls
47 iunss 3945 . . . . . . . . . . . . 13 mrCls mrCls
4847ralbii 2569 . . . . . . . . . . . 12 mrCls mrCls
49 ralcom 2702 . . . . . . . . . . . 12 mrCls mrCls
5048, 49bitri 240 . . . . . . . . . . 11 mrCls mrCls
5146, 50syl6bbr 254 . . . . . . . . . 10 ACS mrCls
52 elrint2 3906 . . . . . . . . . . 11
5352adantl 452 . . . . . . . . . 10 ACS
54 funmpt 5292 . . . . . . . . . . . . 13 mrCls
55 funiunfv 5776 . . . . . . . . . . . . 13 mrCls mrCls mrCls
5654, 55ax-mp 8 . . . . . . . . . . . 12 mrCls mrCls
5756sseq1i 3204 . . . . . . . . . . 11 mrCls mrCls
58 iunss 3945 . . . . . . . . . . . 12 mrCls mrCls
59 inss1 3391 . . . . . . . . . . . . . . . . 17
60 sspwb 4225 . . . . . . . . . . . . . . . . . . 19
6142, 60sylib 188 . . . . . . . . . . . . . . . . . 18
6261adantl 452 . . . . . . . . . . . . . . . . 17 ACS
6359, 62syl5ss 3192 . . . . . . . . . . . . . . . 16 ACS
6463sselda 3182 . . . . . . . . . . . . . . 15 ACS
6524mrcssv 13518 . . . . . . . . . . . . . . . . . . . 20 Moore mrCls
6623, 65syl 15 . . . . . . . . . . . . . . . . . . 19 ACS mrCls
6766ralrimiva 2628 . . . . . . . . . . . . . . . . . 18 ACS mrCls
6867ad2antrr 706 . . . . . . . . . . . . . . . . 17 ACS mrCls
69 iunss 3945 . . . . . . . . . . . . . . . . 17 mrCls mrCls
7068, 69sylibr 203 . . . . . . . . . . . . . . . 16 ACS mrCls
71 ssexg 4162 . . . . . . . . . . . . . . . 16 mrCls mrCls
7270, 13, 71sylancl 643 . . . . . . . . . . . . . . 15 ACS mrCls
73 fveq2 5527 . . . . . . . . . . . . . . . . 17 mrCls mrCls
7473iuneq2d 3932 . . . . . . . . . . . . . . . 16 mrCls mrCls
7574, 33fvmptg 5602 . . . . . . . . . . . . . . 15 mrCls mrCls mrCls
7664, 72, 75syl2anc 642 . . . . . . . . . . . . . 14 ACS mrCls mrCls
7776sseq1d 3207 . . . . . . . . . . . . 13 ACS mrCls mrCls
7877ralbidva 2561 . . . . . . . . . . . 12 ACS mrCls mrCls
7958, 78syl5bb 248 . . . . . . . . . . 11 ACS mrCls mrCls
8057, 79syl5bbr 250 . . . . . . . . . 10 ACS mrCls mrCls
8151, 53, 803bitr4d 276 . . . . . . . . 9 ACS mrCls
8281ralrimiva 2628 . . . . . . . 8 ACS mrCls
8334, 82jca 518 . . . . . . 7 ACS mrCls mrCls
84 feq1 5377 . . . . . . . . 9 mrCls mrCls
85 imaeq1 5009 . . . . . . . . . . . . 13 mrCls mrCls
8685unieqd 3840 . . . . . . . . . . . 12 mrCls mrCls
8786sseq1d 3207 . . . . . . . . . . 11 mrCls mrCls
8887bibi2d 309 . . . . . . . . . 10 mrCls mrCls
8988ralbidv 2565 . . . . . . . . 9 mrCls mrCls
9084, 89anbi12d 691 . . . . . . . 8 mrCls mrCls mrCls
9190spcegv 2871 . . . . . . 7 mrCls mrCls mrCls
9240, 83, 91sylc 56 . . . . . 6 ACS
93 isacs 13555 . . . . . 6 ACS Moore
9420, 92, 93sylanbrc 645 . . . . 5 ACS ACS
9594adantl 452 . . . 4 ACS ACS
9612, 95ismred2 13507 . . 3 ACS Moore
9796trud 1314 . 2 ACS Moore
984, 97vtoclg 2845 1 ACS Moore
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wtru 1307  wex 1530   wceq 1625   wcel 1686  wral 2545  cvv 2790   cin 3153   wss 3154  cpw 3627  cuni 3829  cint 3864  ciun 3907   cmpt 4079   cxp 4689  cima 4694   wfun 5251  wf 5253  cfv 5257  cfn 6865  Moorecmre 13486  mrClscmrc 13487  ACScacs 13489 This theorem is referenced by:  acsfn1  13565  acsfn1c  13566  acsfn2  13567  submacs  14444  subgacs  14654  nsgacs  14655  lssacs  15726  acsfn1p  27518  subrgacs  27519  sdrgacs  27520 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-fv 5265  df-mre 13490  df-mrc 13491  df-acs 13493
 Copyright terms: Public domain W3C validator