Theorem iscnrm3rlem4

Description: Lemma for iscnrm3rlem8 . Given two disjoint subsets S and T of the underlying set of a topology J , if N is a superset of ( ( ( clsJ )S ) \ T ) , then it is a superset of S . (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3rlem4.1	|- ( ph -> J e. Top )
	iscnrm3rlem4.2	|- ( ph -> S C_ U. J )
	iscnrm3rlem4.3	|- ( ph -> ( S i^i T ) = (/) )
	iscnrm3rlem4.4	|- ( ph -> ( ( ( cls ` J ) ` S ) \ T ) C_ N )
Assertion	iscnrm3rlem4	|- ( ph -> S C_ N )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	|- ( ph -> J e. Top )
2		iscnrm3rlem4.2	|- ( ph -> S C_ U. J )
3		iscnrm3rlem4.3	|- ( ph -> ( S i^i T ) = (/) )
4		iscnrm3rlem4.4	|- ( ph -> ( ( ( cls ` J ) ` S ) \ T ) C_ N )
5		indifdi	|- ( S i^i ( ( ( cls ` J ) ` S ) \ T ) ) = ( ( S i^i ( ( cls ` J ) ` S ) ) \ ( S i^i T ) )
6	5	a1i	|- ( ph -> ( S i^i ( ( ( cls ` J ) ` S ) \ T ) ) = ( ( S i^i ( ( cls ` J ) ` S ) ) \ ( S i^i T ) ) )
7	3	difeq2d	|- ( ph -> ( ( S i^i ( ( cls ` J ) ` S ) ) \ ( S i^i T ) ) = ( ( S i^i ( ( cls ` J ) ` S ) ) \ (/) ) )
8		dif0	|- ( ( S i^i ( ( cls ` J ) ` S ) ) \ (/) ) = ( S i^i ( ( cls ` J ) ` S ) )
9	7 8	eqtrdi	|- ( ph -> ( ( S i^i ( ( cls ` J ) ` S ) ) \ ( S i^i T ) ) = ( S i^i ( ( cls ` J ) ` S ) ) )
10		eqid	|- U. J = U. J
11	10	sscls	|- ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
12	1 2 11	syl2anc	|- ( ph -> S C_ ( ( cls ` J ) ` S ) )
13		df-ss	|- ( S C_ ( ( cls ` J ) ` S ) <-> ( S i^i ( ( cls ` J ) ` S ) ) = S )
14	12 13	sylib	|- ( ph -> ( S i^i ( ( cls ` J ) ` S ) ) = S )
15	6 9 14	3eqtrd	|- ( ph -> ( S i^i ( ( ( cls ` J ) ` S ) \ T ) ) = S )
16		df-ss	|- ( S C_ ( ( ( cls ` J ) ` S ) \ T ) <-> ( S i^i ( ( ( cls ` J ) ` S ) \ T ) ) = S )
17	15 16	sylibr	|- ( ph -> S C_ ( ( ( cls ` J ) ` S ) \ T ) )
18	17 4	sstrd	|- ( ph -> S C_ N )