Theorem clss2lem

Description: The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020)

	Ref	Expression
Hypothesis	clss2lem.1	|- ( ph -> ( ch -> ps ) )
Assertion	clss2lem	|- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ |^| { x | ( X C_ x /\ ch ) } )

Proof

Step	Hyp	Ref	Expression
1		clss2lem.1	|- ( ph -> ( ch -> ps ) )
2	1	adantld	|- ( ph -> ( ( X C_ x /\ ch ) -> ps ) )
3	2	alrimiv	|- ( ph -> A. x ( ( X C_ x /\ ch ) -> ps ) )
4		pm5.3	|- ( ( ( X C_ x /\ ch ) -> ps ) <-> ( ( X C_ x /\ ch ) -> ( X C_ x /\ ps ) ) )
5	4	albii	|- ( A. x ( ( X C_ x /\ ch ) -> ps ) <-> A. x ( ( X C_ x /\ ch ) -> ( X C_ x /\ ps ) ) )
6		ss2ab	|- ( { x | ( X C_ x /\ ch ) } C_ { x | ( X C_ x /\ ps ) } <-> A. x ( ( X C_ x /\ ch ) -> ( X C_ x /\ ps ) ) )
7	5 6	bitr4i	|- ( A. x ( ( X C_ x /\ ch ) -> ps ) <-> { x | ( X C_ x /\ ch ) } C_ { x | ( X C_ x /\ ps ) } )
8	3 7	sylib	|- ( ph -> { x | ( X C_ x /\ ch ) } C_ { x | ( X C_ x /\ ps ) } )
9		intss	|- ( { x | ( X C_ x /\ ch ) } C_ { x | ( X C_ x /\ ps ) } -> |^| { x | ( X C_ x /\ ps ) } C_ |^| { x | ( X C_ x /\ ch ) } )
10	8 9	syl	|- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ |^| { x | ( X C_ x /\ ch ) } )