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

Theorem mrcsscl 16261
Description: The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.)
Hypothesis
Ref Expression
mrcfval.f 𝐹 = (mrCls‘𝐶)
Assertion
Ref Expression
mrcsscl ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝐶) → (𝐹𝑈) ⊆ 𝑉)

Proof of Theorem mrcsscl
StepHypRef Expression
1 mress 16234 . . . 4 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑉𝐶) → 𝑉𝑋)
213adant2 1078 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝐶) → 𝑉𝑋)
3 mrcfval.f . . . 4 𝐹 = (mrCls‘𝐶)
43mrcss 16257 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝑋) → (𝐹𝑈) ⊆ (𝐹𝑉))
52, 4syld3an3 1369 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝐶) → (𝐹𝑈) ⊆ (𝐹𝑉))
63mrcid 16254 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑉𝐶) → (𝐹𝑉) = 𝑉)
763adant2 1078 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝐶) → (𝐹𝑉) = 𝑉)
85, 7sseqtrd 3633 1 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑉𝑉𝐶) → (𝐹𝑈) ⊆ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1481  wcel 1988  wss 3567  cfv 5876  Moorecmre 16223  mrClscmrc 16224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-int 4467  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-mre 16227  df-mrc 16228
This theorem is referenced by:  submrc  16269  isacs2  16295  isacs3lem  17147  mrelatlub  17167  mrcmndind  17347  gsumwspan  17364  symggen  17871  cntzspan  18228  dprdspan  18407  subgdmdprd  18414  subgdprd  18415  dprdsn  18416  dprd2dlem1  18421  dprd2da  18422  dmdprdsplit2lem  18425  ablfac1b  18450  pgpfac1lem1  18454  pgpfac1lem5  18459  evlseu  19497  mrccss  20019  ismrcd2  37081  mrefg3  37090  isnacs3  37092
  Copyright terms: Public domain W3C validator