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

Theorem mrcuni 14895
 Description: Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
Hypothesis
Ref Expression
mrcfval.f mrCls
Assertion
Ref Expression
mrcuni Moore

Proof of Theorem mrcuni
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . 3 Moore Moore
2 simpll 753 . . . . . . 7 Moore Moore
3 ssel2 3484 . . . . . . . . 9
43elpwid 4007 . . . . . . . 8
54adantll 713 . . . . . . 7 Moore
6 mrcfval.f . . . . . . . 8 mrCls
76mrcssid 14891 . . . . . . 7 Moore
82, 5, 7syl2anc 661 . . . . . 6 Moore
96mrcf 14883 . . . . . . . . . . 11 Moore
10 ffun 5723 . . . . . . . . . . 11
119, 10syl 16 . . . . . . . . . 10 Moore
1211adantr 465 . . . . . . . . 9 Moore
13 fdm 5725 . . . . . . . . . . . 12
149, 13syl 16 . . . . . . . . . . 11 Moore
1514sseq2d 3517 . . . . . . . . . 10 Moore
1615biimpar 485 . . . . . . . . 9 Moore
17 funfvima2 6133 . . . . . . . . 9
1812, 16, 17syl2anc 661 . . . . . . . 8 Moore
1918imp 429 . . . . . . 7 Moore
20 elssuni 4264 . . . . . . 7
2119, 20syl 16 . . . . . 6 Moore
228, 21sstrd 3499 . . . . 5 Moore
2322ralrimiva 2857 . . . 4 Moore
24 unissb 4266 . . . 4
2523, 24sylibr 212 . . 3 Moore
266mrcssv 14888 . . . . . . 7 Moore
2726adantr 465 . . . . . 6 Moore
2827ralrimivw 2858 . . . . 5 Moore
29 ffn 5721 . . . . . . 7
309, 29syl 16 . . . . . 6 Moore
31 sseq1 3510 . . . . . . 7
3231ralima 6137 . . . . . 6
3330, 32sylan 471 . . . . 5 Moore
3428, 33mpbird 232 . . . 4 Moore
35 unissb 4266 . . . 4
3634, 35sylibr 212 . . 3 Moore
376mrcss 14890 . . 3 Moore
381, 25, 36, 37syl3anc 1229 . 2 Moore
39 simpll 753 . . . . . . . 8 Moore Moore
40 elssuni 4264 . . . . . . . . 9
4140adantl 466 . . . . . . . 8 Moore
42 sspwuni 4401 . . . . . . . . . . 11
4342biimpi 194 . . . . . . . . . 10
4443adantl 466 . . . . . . . . 9 Moore
4544adantr 465 . . . . . . . 8 Moore
466mrcss 14890 . . . . . . . 8 Moore
4739, 41, 45, 46syl3anc 1229 . . . . . . 7 Moore
4847ralrimiva 2857 . . . . . 6 Moore
49 sseq1 3510 . . . . . . . 8
5049ralima 6137 . . . . . . 7
5130, 50sylan 471 . . . . . 6 Moore
5248, 51mpbird 232 . . . . 5 Moore
53 unissb 4266 . . . . 5
5452, 53sylibr 212 . . . 4 Moore
556mrcssv 14888 . . . . 5 Moore
5655adantr 465 . . . 4 Moore
576mrcss 14890 . . . 4 Moore
581, 54, 56, 57syl3anc 1229 . . 3 Moore
596mrcidm 14893 . . . 4 Moore
601, 44, 59syl2anc 661 . . 3 Moore
6158, 60sseqtrd 3525 . 2 Moore
6238, 61eqssd 3506 1 Moore
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1383   wcel 1804  wral 2793   wss 3461  cpw 3997  cuni 4234   cdm 4989  cima 4992   wfun 5572   wfn 5573  wf 5574  cfv 5578  Moorecmre 14856  mrClscmrc 14857 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-int 4272  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-mre 14860  df-mrc 14861 This theorem is referenced by:  mrcun  14896  isacs4lem  15672
 Copyright terms: Public domain W3C validator