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

Theorem isacs2 15637
 Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
Hypothesis
Ref Expression
isacs2.f mrCls
Assertion
Ref Expression
isacs2 ACS Moore
Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem isacs2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isacs 15635 . 2 ACS Moore
2 iunss 4310 . . . . . . . . 9
3 ffun 5742 . . . . . . . . . . 11
4 funiunfv 6171 . . . . . . . . . . 11
53, 4syl 17 . . . . . . . . . 10
65sseq1d 3445 . . . . . . . . 9
72, 6syl5rbbr 268 . . . . . . . 8
87bibi2d 325 . . . . . . 7
98ralbidv 2829 . . . . . 6
109pm5.32i 649 . . . . 5
1110exbii 1726 . . . 4
12 simpll 768 . . . . . . . . . . . . 13 Moore Moore
13 inss1 3643 . . . . . . . . . . . . . . . 16
1413sseli 3414 . . . . . . . . . . . . . . 15
15 elpwi 3951 . . . . . . . . . . . . . . 15
1614, 15syl 17 . . . . . . . . . . . . . 14
1716adantl 473 . . . . . . . . . . . . 13 Moore
18 simplr 770 . . . . . . . . . . . . 13 Moore
19 isacs2.f . . . . . . . . . . . . . 14 mrCls
2019mrcsscl 15604 . . . . . . . . . . . . 13 Moore
2112, 17, 18, 20syl3anc 1292 . . . . . . . . . . . 12 Moore
2221ralrimiva 2809 . . . . . . . . . . 11 Moore
2322adantlr 729 . . . . . . . . . 10 Moore
2423adantllr 733 . . . . . . . . 9 Moore
25 simplll 776 . . . . . . . . . . . . . . . . . 18 Moore Moore
2616adantl 473 . . . . . . . . . . . . . . . . . . 19 Moore
27 elpwi 3951 . . . . . . . . . . . . . . . . . . . 20
2827ad2antlr 741 . . . . . . . . . . . . . . . . . . 19 Moore
2926, 28sstrd 3428 . . . . . . . . . . . . . . . . . 18 Moore
3025, 19, 29mrcssidd 15609 . . . . . . . . . . . . . . . . 17 Moore
31 vex 3034 . . . . . . . . . . . . . . . . . 18
3231elpw 3948 . . . . . . . . . . . . . . . . 17
3330, 32sylibr 217 . . . . . . . . . . . . . . . 16 Moore
34 inss2 3644 . . . . . . . . . . . . . . . . . 18
3534sseli 3414 . . . . . . . . . . . . . . . . 17
3635adantl 473 . . . . . . . . . . . . . . . 16 Moore
3733, 36elind 3609 . . . . . . . . . . . . . . 15 Moore
3819mrccl 15595 . . . . . . . . . . . . . . . . 17 Moore
3925, 29, 38syl2anc 673 . . . . . . . . . . . . . . . 16 Moore
40 mresspw 15576 . . . . . . . . . . . . . . . . . . 19 Moore
4140ad3antrrr 744 . . . . . . . . . . . . . . . . . 18 Moore
4241, 39sseldd 3419 . . . . . . . . . . . . . . . . 17 Moore
43 simprr 774 . . . . . . . . . . . . . . . . . 18 Moore
4443ad2antrr 740 . . . . . . . . . . . . . . . . 17 Moore
45 eleq1 2537 . . . . . . . . . . . . . . . . . . 19
46 pweq 3945 . . . . . . . . . . . . . . . . . . . . 21
4746ineq1d 3624 . . . . . . . . . . . . . . . . . . . 20
48 sseq2 3440 . . . . . . . . . . . . . . . . . . . 20
4947, 48raleqbidv 2987 . . . . . . . . . . . . . . . . . . 19
5045, 49bibi12d 328 . . . . . . . . . . . . . . . . . 18
5150rspcva 3134 . . . . . . . . . . . . . . . . 17
5242, 44, 51syl2anc 673 . . . . . . . . . . . . . . . 16 Moore
5339, 52mpbid 215 . . . . . . . . . . . . . . 15 Moore
54 fveq2 5879 . . . . . . . . . . . . . . . . 17
5554sseq1d 3445 . . . . . . . . . . . . . . . 16
5655rspcva 3134 . . . . . . . . . . . . . . 15
5737, 53, 56syl2anc 673 . . . . . . . . . . . . . 14 Moore
58 sstr2 3425 . . . . . . . . . . . . . 14
5957, 58syl 17 . . . . . . . . . . . . 13 Moore
6059ralimdva 2805 . . . . . . . . . . . 12 Moore
6160imp 436 . . . . . . . . . . 11 Moore
62 fveq2 5879 . . . . . . . . . . . . 13
6362sseq1d 3445 . . . . . . . . . . . 12
6463cbvralv 3005 . . . . . . . . . . 11
6561, 64sylib 201 . . . . . . . . . 10 Moore
66 simplr 770 . . . . . . . . . . 11 Moore
6743ad2antrr 740 . . . . . . . . . . 11 Moore
68 eleq1 2537 . . . . . . . . . . . . 13
69 pweq 3945 . . . . . . . . . . . . . . 15
7069ineq1d 3624 . . . . . . . . . . . . . 14
71 sseq2 3440 . . . . . . . . . . . . . 14
7270, 71raleqbidv 2987 . . . . . . . . . . . . 13
7368, 72bibi12d 328 . . . . . . . . . . . 12
7473rspcva 3134 . . . . . . . . . . 11
7566, 67, 74syl2anc 673 . . . . . . . . . 10 Moore
7665, 75mpbird 240 . . . . . . . . 9 Moore
7724, 76impbida 850 . . . . . . . 8 Moore
7877ralrimiva 2809 . . . . . . 7 Moore
7978ex 441 . . . . . 6 Moore
8079exlimdv 1787 . . . . 5 Moore
8119mrcf 15593 . . . . . . . 8 Moore
8281, 40fssd 5750 . . . . . . 7 Moore
83 fvex 5889 . . . . . . . . 9 mrCls
8419, 83eqeltri 2545 . . . . . . . 8
85 feq1 5720 . . . . . . . . 9
86 fveq1 5878 . . . . . . . . . . . . . . 15
8786sseq1d 3445 . . . . . . . . . . . . . 14
8887ralbidv 2829 . . . . . . . . . . . . 13
89 fveq2 5879 . . . . . . . . . . . . . . 15
9089sseq1d 3445 . . . . . . . . . . . . . 14
9190cbvralv 3005 . . . . . . . . . . . . 13
9288, 91syl6bb 269 . . . . . . . . . . . 12
9392bibi2d 325 . . . . . . . . . . 11
9493ralbidv 2829 . . . . . . . . . 10
95 sseq2 3440 . . . . . . . . . . . . 13
9670, 95raleqbidv 2987 . . . . . . . . . . . 12
9768, 96bibi12d 328 . . . . . . . . . . 11
9897cbvralv 3005 . . . . . . . . . 10
9994, 98syl6bb 269 . . . . . . . . 9
10085, 99anbi12d 725 . . . . . . . 8
10184, 100spcev 3127 . . . . . . 7
10282, 101sylan 479 . . . . . 6 Moore
103102ex 441 . . . . 5 Moore
10480, 103impbid 195 . . . 4 Moore
10511, 104syl5bb 265 . . 3 Moore
106105pm5.32i 649 . 2 Moore Moore
1071, 106bitri 257 1 ACS Moore
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   wceq 1452  wex 1671   wcel 1904  wral 2756  cvv 3031   cin 3389   wss 3390  cpw 3942  cuni 4190  ciun 4269  cima 4842   wfun 5583  wf 5585  cfv 5589  cfn 7587  Moorecmre 15566  mrClscmrc 15567  ACScacs 15569 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-fv 5597  df-mre 15570  df-mrc 15571  df-acs 15573 This theorem is referenced by:  acsfiel  15638  isacs5  16496
 Copyright terms: Public domain W3C validator