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

Theorem clsslem 13060
Description: The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.)
Assertion
Ref Expression
clsslem  |-  ( R 
C_  S  ->  |^| { r  |  ( R  C_  r  /\  ph ) } 
C_  |^| { r  |  ( S  C_  r  /\  ph ) } )
Distinct variable groups:    R, r    S, r
Allowed substitution hint:    ph( r)

Proof of Theorem clsslem
StepHypRef Expression
1 sstr2 3441 . . . 4  |-  ( R 
C_  S  ->  ( S  C_  r  ->  R  C_  r ) )
21anim1d 568 . . 3  |-  ( R 
C_  S  ->  (
( S  C_  r  /\  ph )  ->  ( R  C_  r  /\  ph ) ) )
32ss2abdv 3504 . 2  |-  ( R 
C_  S  ->  { r  |  ( S  C_  r  /\  ph ) } 
C_  { r  |  ( R  C_  r  /\  ph ) } )
4 intss 4258 . 2  |-  ( { r  |  ( S 
C_  r  /\  ph ) }  C_  { r  |  ( R  C_  r  /\  ph ) }  ->  |^| { r  |  ( R  C_  r  /\  ph ) }  C_  |^|
{ r  |  ( S  C_  r  /\  ph ) } )
53, 4syl 17 1  |-  ( R 
C_  S  ->  |^| { r  |  ( R  C_  r  /\  ph ) } 
C_  |^| { r  |  ( S  C_  r  /\  ph ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   {cab 2439    C_ wss 3406   |^|cint 4237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-in 3413  df-ss 3420  df-int 4238
This theorem is referenced by:  trclsslem  13066
  Copyright terms: Public domain W3C validator