Metamath Proof Explorer


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 φ J Top
iscnrm3rlem4.2 φ S J
iscnrm3rlem4.3 φ S T =
iscnrm3rlem4.4 φ cls J S T N
Assertion iscnrm3rlem4 φ S N

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 φ J Top
2 iscnrm3rlem4.2 φ S J
3 iscnrm3rlem4.3 φ S T =
4 iscnrm3rlem4.4 φ cls J S T N
5 indifdi S cls J S T = S cls J S S T
6 5 a1i φ S cls J S T = S cls J S S T
7 3 difeq2d φ S cls J S S T = S cls J S
8 dif0 S cls J S = S cls J S
9 7 8 eqtrdi φ S cls J S S T = S cls J S
10 eqid J = J
11 10 sscls J Top S J S cls J S
12 1 2 11 syl2anc φ S cls J S
13 df-ss S cls J S S cls J S = S
14 12 13 sylib φ S cls J S = S
15 6 9 14 3eqtrd φ S cls J S T = S
16 df-ss S cls J S T S cls J S T = S
17 15 16 sylibr φ S cls J S T
18 17 4 sstrd φ S N