Metamath Proof Explorer

Theorem iscnrm3r

Description: Lemma for iscnrm3 . If all subspaces of a topology are normal, i.e., two disjoint closed sets can be separated by open neighborhoods, then in the original topology two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3r 
|- ( J e. Top -> ( A. z e. ~P U. J A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> ( ( S e. ~P U. J /\ T e. ~P U. J ) -> ( ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( J |`t z ) = ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
2 1 fveq2d 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( Clsd ` ( J |`t z ) ) = ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) )
3 1 rexeqdv 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) <-> E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) )
4 1 3 rexeqbidv 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) <-> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) )
5 4 imbi2d 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) <-> ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) ) )
6 2 5 raleqbidv 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) <-> A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) ) )
7 2 6 raleqbidv 
 |-  ( z = ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) -> ( A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) <-> A. c e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) ) )
8 7 rspcv 
 |-  ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J -> ( A. z e. ~P U. J A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> A. c e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) ) )
9 8 3ad2ant1 
 |-  ( ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) -> ( A. z e. ~P U. J A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> A. c e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) ) )
10 ineq12 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( c i^i d ) = ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) )
11 10 eqeq1d 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( ( c i^i d ) = (/) <-> ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) ) )
12 simpl 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) )
13 12 sseq1d 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( c C_ l <-> ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l ) )
14 simpr 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) )
15 14 sseq1d 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( d C_ k <-> ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k ) )
16 13 15 3anbi12d 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) <-> ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) )
17 16 2rexbidv 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) <-> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) )
18 11 17 imbi12d 
 |-  ( ( c = ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) /\ d = ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) -> ( ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) <-> ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) ) )
19 18 rspc2gv 
 |-  ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) -> ( A. c e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) ) )
20 19 3adant1 
 |-  ( ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) -> ( A. c e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) A. d e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) ) )
21 9 20 syld 
 |-  ( ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) -> ( A. z e. ~P U. J A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) ) )
22 iscnrm3rlem3 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) )
23 22 3adant3 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) -> ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) )
24 disjdifb 
 |-  ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/)
25 24 a1i 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) -> ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) )
26 iscnrm3rlem8 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) -> ( E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) )
27 25 26 embantd 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) -> ( ( ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) i^i ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) ) = (/) -> E. l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) E. k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ( ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k /\ ( l i^i k ) = (/) ) ) -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) )
28 21 23 27 iscnrm3lem4 
 |-  ( J e. Top -> ( A. z e. ~P U. J A. c e. ( Clsd ` ( J |`t z ) ) A. d e. ( Clsd ` ( J |`t z ) ) ( ( c i^i d ) = (/) -> E. l e. ( J |`t z ) E. k e. ( J |`t z ) ( c C_ l /\ d C_ k /\ ( l i^i k ) = (/) ) ) -> ( ( S e. ~P U. J /\ T e. ~P U. J ) -> ( ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) ) ) )