Metamath Proof Explorer


Theorem clsslem

Description: The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020)

Ref Expression
Assertion clsslem
|- ( R C_ S -> |^| { r | ( R C_ r /\ ph ) } C_ |^| { r | ( S C_ r /\ ph ) } )

Proof

Step Hyp Ref Expression
1 sstr2
 |-  ( R C_ S -> ( S C_ r -> R C_ r ) )
2 1 anim1d
 |-  ( R C_ S -> ( ( S C_ r /\ ph ) -> ( R C_ r /\ ph ) ) )
3 2 ss2abdv
 |-  ( R C_ S -> { r | ( S C_ r /\ ph ) } C_ { r | ( R C_ r /\ ph ) } )
4 intss
 |-  ( { r | ( S C_ r /\ ph ) } C_ { r | ( R C_ r /\ ph ) } -> |^| { r | ( R C_ r /\ ph ) } C_ |^| { r | ( S C_ r /\ ph ) } )
5 3 4 syl
 |-  ( R C_ S -> |^| { r | ( R C_ r /\ ph ) } C_ |^| { r | ( S C_ r /\ ph ) } )