Metamath Proof Explorer

Theorem iscnrm3l

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

Ref Expression
Assertion 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 ) = (/) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( s = C /\ t = D ) -> s = C )
2 simpr 
 |-  ( ( s = C /\ t = D ) -> t = D )
3 2 fveq2d 
 |-  ( ( s = C /\ t = D ) -> ( ( cls ` J ) ` t ) = ( ( cls ` J ) ` D ) )
4 1 3 ineq12d 
 |-  ( ( s = C /\ t = D ) -> ( s i^i ( ( cls ` J ) ` t ) ) = ( C i^i ( ( cls ` J ) ` D ) ) )
5 4 eqeq1d 
 |-  ( ( s = C /\ t = D ) -> ( ( s i^i ( ( cls ` J ) ` t ) ) = (/) <-> ( C i^i ( ( cls ` J ) ` D ) ) = (/) ) )
6 1 fveq2d 
 |-  ( ( s = C /\ t = D ) -> ( ( cls ` J ) ` s ) = ( ( cls ` J ) ` C ) )
7 6 2 ineq12d 
 |-  ( ( s = C /\ t = D ) -> ( ( ( cls ` J ) ` s ) i^i t ) = ( ( ( cls ` J ) ` C ) i^i D ) )
8 7 eqeq1d 
 |-  ( ( s = C /\ t = D ) -> ( ( ( ( cls ` J ) ` s ) i^i t ) = (/) <-> ( ( ( cls ` J ) ` C ) i^i D ) = (/) ) )
9 5 8 anbi12d 
 |-  ( ( s = C /\ t = D ) -> ( ( ( s i^i ( ( cls ` J ) ` t ) ) = (/) /\ ( ( ( cls ` J ) ` s ) i^i t ) = (/) ) <-> ( ( C i^i ( ( cls ` J ) ` D ) ) = (/) /\ ( ( ( cls ` J ) ` C ) i^i D ) = (/) ) ) )
10 1 sseq1d 
 |-  ( ( s = C /\ t = D ) -> ( s C_ n <-> C C_ n ) )
11 2 sseq1d 
 |-  ( ( s = C /\ t = D ) -> ( t C_ m <-> D C_ m ) )
12 10 11 3anbi12d 
 |-  ( ( s = C /\ t = D ) -> ( ( s C_ n /\ t C_ m /\ ( n i^i m ) = (/) ) <-> ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) )
13 12 2rexbidv 
 |-  ( ( s = C /\ t = D ) -> ( E. n e. J E. m e. J ( s C_ n /\ t C_ m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) )
14 iscnrm3llem1 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( C e. ~P U. J /\ D e. ~P U. J ) )
15 simp1 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> J e. Top )
16 eqidd 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> U. J = U. J )
17 simp21 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> Z e. ~P U. J )
18 17 elpwid 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> Z C_ U. J )
19 eqidd 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( J |`t Z ) = ( J |`t Z ) )
20 simp22 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> C e. ( Clsd ` ( J |`t Z ) ) )
21 simp3 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( C i^i D ) = (/) )
22 simp23 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> D e. ( Clsd ` ( J |`t Z ) ) )
23 15 16 18 19 20 21 22 restclssep 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( ( C i^i ( ( cls ` J ) ` D ) ) = (/) /\ ( ( ( cls ` J ) ` C ) i^i D ) = (/) ) )
24 iscnrm3llem2 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( E. n e. J E. m e. J ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) -> E. l e. ( J |`t Z ) E. k e. ( J |`t Z ) ( C C_ l /\ D C_ k /\ ( l i^i k ) = (/) ) ) )
25 23 24 embantd 
 |-  ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) -> ( ( ( ( C i^i ( ( cls ` J ) ` D ) ) = (/) /\ ( ( ( cls ` J ) ` C ) i^i D ) = (/) ) -> E. n e. J E. m e. J ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> E. l e. ( J |`t Z ) E. k e. ( J |`t Z ) ( C C_ l /\ D C_ k /\ ( l i^i k ) = (/) ) ) )
26 9 13 14 25 iscnrm3lem5 
 |-  ( 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 ) = (/) ) ) ) ) )