Metamath Proof Explorer

Theorem iscnrm3llem2

Description: Lemma for iscnrm3l . If there exist disjoint open neighborhoods in the original topology for two disjoint closed sets in a subspace, then they can be separated by open neighborhoods in the subspace topology. (Could shorten proof with ssin0 .) (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( l = ( n i^i Z ) -> ( C C_ l <-> C C_ ( n i^i Z ) ) )
2 ineq1 
 |-  ( l = ( n i^i Z ) -> ( l i^i k ) = ( ( n i^i Z ) i^i k ) )
3 2 eqeq1d 
 |-  ( l = ( n i^i Z ) -> ( ( l i^i k ) = (/) <-> ( ( n i^i Z ) i^i k ) = (/) ) )
4 1 3 3anbi13d 
 |-  ( l = ( n i^i Z ) -> ( ( C C_ l /\ D C_ k /\ ( l i^i k ) = (/) ) <-> ( C C_ ( n i^i Z ) /\ D C_ k /\ ( ( n i^i Z ) i^i k ) = (/) ) ) )
5 sseq2 
 |-  ( k = ( m i^i Z ) -> ( D C_ k <-> D C_ ( m i^i Z ) ) )
6 ineq2 
 |-  ( k = ( m i^i Z ) -> ( ( n i^i Z ) i^i k ) = ( ( n i^i Z ) i^i ( m i^i Z ) ) )
7 6 eqeq1d 
 |-  ( k = ( m i^i Z ) -> ( ( ( n i^i Z ) i^i k ) = (/) <-> ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) ) )
8 5 7 3anbi23d 
 |-  ( k = ( m i^i Z ) -> ( ( C C_ ( n i^i Z ) /\ D C_ k /\ ( ( n i^i Z ) i^i k ) = (/) ) <-> ( C C_ ( n i^i Z ) /\ D C_ ( m i^i Z ) /\ ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) ) ) )
9 simp11 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> J e. Top )
10 simp121 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> Z e. ~P U. J )
11 simp2l 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> n e. J )
12 elrestr 
 |-  ( ( J e. Top /\ Z e. ~P U. J /\ n e. J ) -> ( n i^i Z ) e. ( J |`t Z ) )
13 9 10 11 12 syl3anc 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( n i^i Z ) e. ( J |`t Z ) )
14 simp2r 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> m e. J )
15 elrestr 
 |-  ( ( J e. Top /\ Z e. ~P U. J /\ m e. J ) -> ( m i^i Z ) e. ( J |`t Z ) )
16 9 10 14 15 syl3anc 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( m i^i Z ) e. ( J |`t Z ) )
17 simp31 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> C C_ n )
18 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 ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> U. J = U. J )
19 10 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 ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> Z C_ U. J )
20 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 ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( J |`t Z ) = ( J |`t Z ) )
21 simp122 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> C e. ( Clsd ` ( J |`t Z ) ) )
22 9 18 19 20 21 restcls2lem 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> C C_ Z )
23 17 22 ssind 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> C C_ ( n i^i Z ) )
24 simp32 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> D C_ m )
25 simp123 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> D e. ( Clsd ` ( J |`t Z ) ) )
26 9 18 19 20 25 restcls2lem 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> D C_ Z )
27 24 26 ssind 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> D C_ ( m i^i Z ) )
28 inss1 
 |-  ( n i^i Z ) C_ n
29 inss1 
 |-  ( m i^i Z ) C_ m
30 ss2in 
 |-  ( ( ( n i^i Z ) C_ n /\ ( m i^i Z ) C_ m ) -> ( ( n i^i Z ) i^i ( m i^i Z ) ) C_ ( n i^i m ) )
31 28 29 30 mp2an 
 |-  ( ( n i^i Z ) i^i ( m i^i Z ) ) C_ ( n i^i m )
32 simp33 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( n i^i m ) = (/) )
33 31 32 sseqtrid 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( n i^i Z ) i^i ( m i^i Z ) ) C_ (/) )
34 ss0 
 |-  ( ( ( n i^i Z ) i^i ( m i^i Z ) ) C_ (/) -> ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) )
35 33 34 syl 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) )
36 23 27 35 3jca 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( C C_ ( n i^i Z ) /\ D C_ ( m i^i Z ) /\ ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) ) )
37 13 16 36 3jca 
 |-  ( ( ( J e. Top /\ ( Z e. ~P U. J /\ C e. ( Clsd ` ( J |`t Z ) ) /\ D e. ( Clsd ` ( J |`t Z ) ) ) /\ ( C i^i D ) = (/) ) /\ ( n e. J /\ m e. J ) /\ ( C C_ n /\ D C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( n i^i Z ) e. ( J |`t Z ) /\ ( m i^i Z ) e. ( J |`t Z ) /\ ( C C_ ( n i^i Z ) /\ D C_ ( m i^i Z ) /\ ( ( n i^i Z ) i^i ( m i^i Z ) ) = (/) ) ) )
38 4 8 37 iscnrm3lem7 
 |-  ( ( 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 ) = (/) ) ) )