Metamath Proof Explorer

Theorem iscnrm4

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

Ref Expression
Assertion iscnrm4 
|- ( 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. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) = (/) ) ) ) )
2 id 
 |-  ( J e. Top -> J e. Top )
3 2 sepnsepo 
 |-  ( J e. Top -> ( E. n e. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) <-> E. n e. J E. m e. J ( s C_ n /\ t C_ m /\ ( n i^i m ) = (/) ) ) )
4 3 imbi2d 
 |-  ( J e. Top -> ( ( ( ( s i^i ( ( cls ` J ) ` t ) ) = (/) /\ ( ( ( cls ` J ) ` s ) i^i t ) = (/) ) -> E. n e. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) ) <-> ( ( ( 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 ) = (/) ) ) ) )
5 4 2ralbidv 
 |-  ( 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. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) ) <-> 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 ) = (/) ) ) ) )
6 5 pm5.32i 
 |-  ( ( 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. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) ) ) <-> ( 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 ) = (/) ) ) ) )
7 1 6 bitr4i 
 |-  ( 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. ( ( nei ` J ) ` s ) E. m e. ( ( nei ` J ) ` t ) ( n i^i m ) = (/) ) ) )