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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
	iscnrm3rlem4.3	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
	iscnrm3rlem4.4	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ⊆ 𝑁 )
Assertion	iscnrm3rlem4	⊢ ( 𝜑 → 𝑆 ⊆ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3		iscnrm3rlem4.3	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
4		iscnrm3rlem4.4	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ⊆ 𝑁 )
5		indifdi	⊢ ( 𝑆 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ) = ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ( 𝑆 ∩ 𝑇 ) )
6	5	a1i	⊢ ( 𝜑 → ( 𝑆 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ) = ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ( 𝑆 ∩ 𝑇 ) ) )
7	3	difeq2d	⊢ ( 𝜑 → ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ( 𝑆 ∩ 𝑇 ) ) = ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ∅ ) )
8		dif0	⊢ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ∅ ) = ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
9	7 8	eqtrdi	⊢ ( 𝜑 → ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∖ ( 𝑆 ∩ 𝑇 ) ) = ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
10		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
11	10	sscls	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
12	1 2 11	syl2anc	⊢ ( 𝜑 → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
13		df-ss	⊢ ( 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = 𝑆 )
14	12 13	sylib	⊢ ( 𝜑 → ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = 𝑆 )
15	6 9 14	3eqtrd	⊢ ( 𝜑 → ( 𝑆 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ) = 𝑆 )
16		df-ss	⊢ ( 𝑆 ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ↔ ( 𝑆 ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ) = 𝑆 )
17	15 16	sylibr	⊢ ( 𝜑 → 𝑆 ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) )
18	17 4	sstrd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑁 )