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	$$⊢\phi \to J\in \mathrm{Top}$$
	iscnrm3rlem4.2	$$⊢\phi \to S\subseteq \bigcup J$$
	iscnrm3rlem4.3	$$⊢\phi \to S\cap T=\varnothing$$
	iscnrm3rlem4.4	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\setminus T\subseteq N$$
Assertion	iscnrm3rlem4	$$⊢\phi \to S\subseteq N$$

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		iscnrm3rlem4.2	$$⊢\phi \to S\subseteq \bigcup J$$
3		iscnrm3rlem4.3	$$⊢\phi \to S\cap T=\varnothing$$
4		iscnrm3rlem4.4	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\setminus T\subseteq N$$
5		indifdi	$$⊢S\cap \left(\mathrm{cls}\left(J\right)\left(S\right)\setminus T\right)=\left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \left(S\cap T\right)$$
6	5	a1i	$$⊢\phi \to S\cap \left(\mathrm{cls}\left(J\right)\left(S\right)\setminus T\right)=\left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \left(S\cap T\right)$$
7	3	difeq2d	$$⊢\phi \to \left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \left(S\cap T\right)=\left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \varnothing$$
8		dif0	$$⊢\left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \varnothing =S\cap \mathrm{cls}\left(J\right)\left(S\right)$$
9	7 8	eqtrdi	$$⊢\phi \to \left(S\cap \mathrm{cls}\left(J\right)\left(S\right)\right)\setminus \left(S\cap T\right)=S\cap \mathrm{cls}\left(J\right)\left(S\right)$$
10		eqid	$$⊢\bigcup J=\bigcup J$$
11	10	sscls	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq \bigcup J\right)\to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$
12	1 2 11	syl2anc	$$⊢\phi \to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$
13		dfss2	$$⊢S\subseteq \mathrm{cls}\left(J\right)\left(S\right)\leftrightarrow S\cap \mathrm{cls}\left(J\right)\left(S\right)=S$$
14	12 13	sylib	$$⊢\phi \to S\cap \mathrm{cls}\left(J\right)\left(S\right)=S$$
15	6 9 14	3eqtrd	$$⊢\phi \to S\cap \left(\mathrm{cls}\left(J\right)\left(S\right)\setminus T\right)=S$$
16		dfss2	$$⊢S\subseteq \mathrm{cls}\left(J\right)\left(S\right)\setminus T\leftrightarrow S\cap \left(\mathrm{cls}\left(J\right)\left(S\right)\setminus T\right)=S$$
17	15 16	sylibr	$$⊢\phi \to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)\setminus T$$
18	17 4	sstrd	$$⊢\phi \to S\subseteq N$$