Metamath Proof Explorer

Theorem iscnrm3

Description: A completely normal topology is a topology in which two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3 
|- ( J e. CNrm <-> ( J e. Top /\ A. s e. ~P U. J A. 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 eqid 
 |-  U. J = U. J
2 1 iscnrm 
 |-  ( J e. CNrm <-> ( J e. Top /\ A. z e. ~P U. J ( J |`t z ) e. Nrm ) )
3 iscnrm3lem1 
 |-  ( 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 ) = (/) ) ) <-> A. z e. ~P U. J ( ( J |`t z ) e. Top /\ 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 ) = (/) ) ) ) ) )
4 isnrm3 
 |-  ( ( J |`t z ) e. Nrm <-> ( ( J |`t z ) e. Top /\ 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 ) = (/) ) ) ) )
5 4 ralbii 
 |-  ( A. z e. ~P U. J ( J |`t z ) e. Nrm <-> A. z e. ~P U. J ( ( J |`t z ) e. Top /\ 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 ) = (/) ) ) ) )
6 3 5 bitr4di 
 |-  ( 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 ) = (/) ) ) <-> A. z e. ~P U. J ( J |`t z ) e. Nrm ) )
7 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 ) = (/) ) ) ) ) )
8 iscnrm3l 
 |-  ( J e. Top -> ( A. s e. ~P U. J A. 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 ) = (/) ) ) -> ( ( z e. ~P U. J /\ c e. ( Clsd ` ( J |`t z ) ) /\ 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 ) = (/) ) ) ) ) )
9 7 8 iscnrm3lem2 
 |-  ( 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 ) = (/) ) ) <-> A. s e. ~P U. J A. 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 ) = (/) ) ) ) )
10 6 9 bitr3d 
 |-  ( J e. Top -> ( A. z e. ~P U. J ( J |`t z ) e. Nrm <-> A. s e. ~P U. J A. 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 ) = (/) ) ) ) )
11 10 pm5.32i 
 |-  ( ( J e. Top /\ A. z e. ~P U. J ( J |`t z ) e. Nrm ) <-> ( J e. Top /\ A. s e. ~P U. J A. 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 ) = (/) ) ) ) )
12 2 11 bitri 
 |-  ( J e. CNrm <-> ( J e. Top /\ A. s e. ~P U. J A. 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 ) = (/) ) ) ) )