MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mrcuni Structured version   Visualization version   GIF version
Theorem mrcuni 17561
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 483 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ 𝐢 ∈ (Mooreβ€˜π‘‹))
2 simpll 765 . . . . . . 7 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ 𝐢 ∈ (Mooreβ€˜π‘‹))
3 ssel2 3976 . . . . . . . . 9 ((π‘ˆ βŠ† 𝒫 𝑋 ∧ 𝑠 ∈ π‘ˆ) β†’ 𝑠 ∈ 𝒫 𝑋)
43elpwid 4610 . . . . . . . 8 ((π‘ˆ βŠ† 𝒫 𝑋 ∧ 𝑠 ∈ π‘ˆ) β†’ 𝑠 βŠ† 𝑋)
54adantll 712 . . . . . . 7 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ 𝑠 βŠ† 𝑋)
6 mrcfval.f . . . . . . . 8 𝐹 = (mrClsβ€˜πΆ)
76mrcssid 17557 . . . . . . 7 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ 𝑠 βŠ† 𝑋) β†’ 𝑠 βŠ† (πΉβ€˜π‘ ))
82, 5, 7syl2anc 584 . . . . . 6 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ 𝑠 βŠ† (πΉβ€˜π‘ ))
96mrcf 17549 . . . . . . . . . . 11 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ 𝐹:𝒫 π‘‹βŸΆπΆ)
109ffund 6718 . . . . . . . . . 10 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ Fun 𝐹)
1110adantr 481 . . . . . . . . 9 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ Fun 𝐹)
129fdmd 6725 . . . . . . . . . . 11 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ dom 𝐹 = 𝒫 𝑋)
1312sseq2d 4013 . . . . . . . . . 10 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ (π‘ˆ βŠ† dom 𝐹 ↔ π‘ˆ βŠ† 𝒫 𝑋))
1413biimpar 478 . . . . . . . . 9 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ π‘ˆ βŠ† dom 𝐹)
15 funfvima2 7229 . . . . . . . . 9 ((Fun 𝐹 ∧ π‘ˆ βŠ† dom 𝐹) β†’ (𝑠 ∈ π‘ˆ β†’ (πΉβ€˜π‘ ) ∈ (𝐹 β€œ π‘ˆ)))
1611, 14, 15syl2anc 584 . . . . . . . 8 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (𝑠 ∈ π‘ˆ β†’ (πΉβ€˜π‘ ) ∈ (𝐹 β€œ π‘ˆ)))
1716imp 407 . . . . . . 7 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ (πΉβ€˜π‘ ) ∈ (𝐹 β€œ π‘ˆ))
18 elssuni 4940 . . . . . . 7 ((πΉβ€˜π‘ ) ∈ (𝐹 β€œ π‘ˆ) β†’ (πΉβ€˜π‘ ) βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
1917, 18syl 17 . . . . . 6 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ (πΉβ€˜π‘ ) βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
208, 19sstrd 3991 . . . . 5 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ 𝑠 ∈ π‘ˆ) β†’ 𝑠 βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
2120ralrimiva 3146 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆ€π‘  ∈ π‘ˆ 𝑠 βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
22 unissb 4942 . . . 4 (βˆͺ π‘ˆ βŠ† βˆͺ (𝐹 β€œ π‘ˆ) ↔ βˆ€π‘  ∈ π‘ˆ 𝑠 βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
2321, 22sylibr 233 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆͺ π‘ˆ βŠ† βˆͺ (𝐹 β€œ π‘ˆ))
246mrcssv 17554 . . . . . . 7 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ (πΉβ€˜π‘₯) βŠ† 𝑋)
2524adantr 481 . . . . . 6 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜π‘₯) βŠ† 𝑋)
2625ralrimivw 3150 . . . . 5 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† 𝑋)
279ffnd 6715 . . . . . 6 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ 𝐹 Fn 𝒫 𝑋)
28 sseq1 4006 . . . . . . 7 (𝑠 = (πΉβ€˜π‘₯) β†’ (𝑠 βŠ† 𝑋 ↔ (πΉβ€˜π‘₯) βŠ† 𝑋))
2928ralima 7236 . . . . . 6 ((𝐹 Fn 𝒫 𝑋 ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† 𝑋 ↔ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† 𝑋))
3027, 29sylan 580 . . . . 5 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† 𝑋 ↔ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† 𝑋))
3126, 30mpbird 256 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† 𝑋)
32 unissb 4942 . . . 4 (βˆͺ (𝐹 β€œ π‘ˆ) βŠ† 𝑋 ↔ βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† 𝑋)
3331, 32sylibr 233 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆͺ (𝐹 β€œ π‘ˆ) βŠ† 𝑋)
346mrcss 17556 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ βˆͺ π‘ˆ βŠ† βˆͺ (𝐹 β€œ π‘ˆ) ∧ βˆͺ (𝐹 β€œ π‘ˆ) βŠ† 𝑋) β†’ (πΉβ€˜βˆͺ π‘ˆ) βŠ† (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)))
351, 23, 33, 34syl3anc 1371 . 2 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜βˆͺ π‘ˆ) βŠ† (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)))
36 simpll 765 . . . . . . . 8 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ π‘₯ ∈ π‘ˆ) β†’ 𝐢 ∈ (Mooreβ€˜π‘‹))
37 elssuni 4940 . . . . . . . . 9 (π‘₯ ∈ π‘ˆ β†’ π‘₯ βŠ† βˆͺ π‘ˆ)
3837adantl 482 . . . . . . . 8 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ π‘₯ ∈ π‘ˆ) β†’ π‘₯ βŠ† βˆͺ π‘ˆ)
39 sspwuni 5102 . . . . . . . . . . 11 (π‘ˆ βŠ† 𝒫 𝑋 ↔ βˆͺ π‘ˆ βŠ† 𝑋)
4039biimpi 215 . . . . . . . . . 10 (π‘ˆ βŠ† 𝒫 𝑋 β†’ βˆͺ π‘ˆ βŠ† 𝑋)
4140adantl 482 . . . . . . . . 9 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆͺ π‘ˆ βŠ† 𝑋)
4241adantr 481 . . . . . . . 8 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ π‘₯ ∈ π‘ˆ) β†’ βˆͺ π‘ˆ βŠ† 𝑋)
436mrcss 17556 . . . . . . . 8 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘₯ βŠ† βˆͺ π‘ˆ ∧ βˆͺ π‘ˆ βŠ† 𝑋) β†’ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ))
4436, 38, 42, 43syl3anc 1371 . . . . . . 7 (((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) ∧ π‘₯ ∈ π‘ˆ) β†’ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ))
4544ralrimiva 3146 . . . . . 6 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ))
46 sseq1 4006 . . . . . . . 8 (𝑠 = (πΉβ€˜π‘₯) β†’ (𝑠 βŠ† (πΉβ€˜βˆͺ π‘ˆ) ↔ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ)))
4746ralima 7236 . . . . . . 7 ((𝐹 Fn 𝒫 𝑋 ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† (πΉβ€˜βˆͺ π‘ˆ) ↔ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ)))
4827, 47sylan 580 . . . . . 6 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† (πΉβ€˜βˆͺ π‘ˆ) ↔ βˆ€π‘₯ ∈ π‘ˆ (πΉβ€˜π‘₯) βŠ† (πΉβ€˜βˆͺ π‘ˆ)))
4945, 48mpbird 256 . . . . 5 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† (πΉβ€˜βˆͺ π‘ˆ))
50 unissb 4942 . . . . 5 (βˆͺ (𝐹 β€œ π‘ˆ) βŠ† (πΉβ€˜βˆͺ π‘ˆ) ↔ βˆ€π‘  ∈ (𝐹 β€œ π‘ˆ)𝑠 βŠ† (πΉβ€˜βˆͺ π‘ˆ))
5149, 50sylibr 233 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ βˆͺ (𝐹 β€œ π‘ˆ) βŠ† (πΉβ€˜βˆͺ π‘ˆ))
526mrcssv 17554 . . . . 5 (𝐢 ∈ (Mooreβ€˜π‘‹) β†’ (πΉβ€˜βˆͺ π‘ˆ) βŠ† 𝑋)
5352adantr 481 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜βˆͺ π‘ˆ) βŠ† 𝑋)
546mrcss 17556 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ βˆͺ (𝐹 β€œ π‘ˆ) βŠ† (πΉβ€˜βˆͺ π‘ˆ) ∧ (πΉβ€˜βˆͺ π‘ˆ) βŠ† 𝑋) β†’ (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)) βŠ† (πΉβ€˜(πΉβ€˜βˆͺ π‘ˆ)))
551, 51, 53, 54syl3anc 1371 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)) βŠ† (πΉβ€˜(πΉβ€˜βˆͺ π‘ˆ)))
566mrcidm 17559 . . . 4 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ βˆͺ π‘ˆ βŠ† 𝑋) β†’ (πΉβ€˜(πΉβ€˜βˆͺ π‘ˆ)) = (πΉβ€˜βˆͺ π‘ˆ))
571, 41, 56syl2anc 584 . . 3 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜(πΉβ€˜βˆͺ π‘ˆ)) = (πΉβ€˜βˆͺ π‘ˆ))
5855, 57sseqtrd 4021 . 2 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)) βŠ† (πΉβ€˜βˆͺ π‘ˆ))
5935, 58eqssd 3998 1 ((𝐢 ∈ (Mooreβ€˜π‘‹) ∧ π‘ˆ βŠ† 𝒫 𝑋) β†’ (πΉβ€˜βˆͺ π‘ˆ) = (πΉβ€˜βˆͺ (𝐹 β€œ π‘ˆ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061   βŠ† wss 3947  π’« cpw 4601  βˆͺ cuni 4907  dom cdm 5675   β€œ cima 5678  Fun wfun 6534   Fn wfn 6535  β€˜cfv 6540  Moorecmre 17522  mrClscmrc 17523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-mre 17526  df-mrc 17527
This theorem is referenced by:  mrcun  17562  isacs4lem  18493
  Copyright terms: Public domain W3C validator