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 ( 𝑅𝑆 { 𝑟 ∣ ( 𝑅𝑟𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑆𝑟𝜑 ) } )

Proof

Step Hyp Ref Expression
1 sstr2 ( 𝑅𝑆 → ( 𝑆𝑟𝑅𝑟 ) )
2 1 anim1d ( 𝑅𝑆 → ( ( 𝑆𝑟𝜑 ) → ( 𝑅𝑟𝜑 ) ) )
3 2 ss2abdv ( 𝑅𝑆 → { 𝑟 ∣ ( 𝑆𝑟𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑅𝑟𝜑 ) } )
4 intss ( { 𝑟 ∣ ( 𝑆𝑟𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑅𝑟𝜑 ) } → { 𝑟 ∣ ( 𝑅𝑟𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑆𝑟𝜑 ) } )
5 3 4 syl ( 𝑅𝑆 { 𝑟 ∣ ( 𝑅𝑟𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑆𝑟𝜑 ) } )