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 ) } ) |
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 ) } ) |