Metamath Proof Explorer

Theorem iscnrm3rlem8

Description: Lemma for iscnrm3r . Disjoint open neighborhoods in the subspace topology are disjoint open neighborhoods in the original topology given that the subspace is an open set in the original topology. Therefore, given any two sets separated in the original topology and separated by open neighborhoods in the subspace topology, they must be separated by open neighborhoods in the original topology. (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( n = l -> ( S C_ n <-> S C_ l ) )
2 ineq1 
 |-  ( n = l -> ( n i^i m ) = ( l i^i m ) )
3 2 eqeq1d 
 |-  ( n = l -> ( ( n i^i m ) = (/) <-> ( l i^i m ) = (/) ) )
4 1 3 3anbi13d 
 |-  ( n = l -> ( ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) <-> ( S C_ l /\ T C_ m /\ ( l i^i m ) = (/) ) ) )
5 sseq2 
 |-  ( m = k -> ( T C_ m <-> T C_ k ) )
6 ineq2 
 |-  ( m = k -> ( l i^i m ) = ( l i^i k ) )
7 6 eqeq1d 
 |-  ( m = k -> ( ( l i^i m ) = (/) <-> ( l i^i k ) = (/) ) )
8 5 7 3anbi23d 
 |-  ( m = k -> ( ( S C_ l /\ T C_ m /\ ( l i^i m ) = (/) ) <-> ( S C_ l /\ T C_ k /\ ( l i^i k ) = (/) ) ) )
9 simp11 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> J e. Top )
10 simp12l 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> S e. ~P U. J )
11 10 elpwid 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> S C_ U. J )
12 simp12r 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> T e. ~P U. J )
13 12 elpwid 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> T C_ U. J )
14 simp2l 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
15 9 11 13 14 iscnrm3rlem7 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> l e. J )
16 simp2r 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> k e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) )
17 9 11 13 16 iscnrm3rlem7 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> k e. J )
18 simp13l 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( S i^i ( ( cls ` J ) ` T ) ) = (/) )
19 simp31 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) C_ l )
20 9 11 18 19 iscnrm3rlem4 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> S C_ l )
21 incom 
 |-  ( ( ( cls ` J ) ` S ) i^i T ) = ( T i^i ( ( cls ` J ) ` S ) )
22 simp13r 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )
23 21 22 eqtr3id 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( T i^i ( ( cls ` J ) ` S ) ) = (/) )
24 simp32 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) C_ k )
25 9 13 23 24 iscnrm3rlem4 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> T C_ k )
26 simp33 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( l i^i k ) = (/) )
27 20 25 26 3jca 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( S C_ l /\ T C_ k /\ ( l i^i k ) = (/) ) )
28 15 17 27 3jca 
 |-  ( ( ( 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 ) = (/) ) ) /\ ( l e. ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) /\ 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 ) = (/) ) ) -> ( l e. J /\ k e. J /\ ( S C_ l /\ T C_ k /\ ( l i^i k ) = (/) ) ) )
29 4 8 28 iscnrm3lem7 
 |-  ( ( 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 ) = (/) ) ) )