Metamath Proof Explorer

Theorem iscnrm3rlem3

Description: Lemma for iscnrm3r . The designed subspace is a subset of the original set; the two sets are closed sets in the subspace. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3rlem3 
|- ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 uniexg 
 |-  ( J e. Top -> U. J e. _V )
2 difssd 
 |-  ( J e. Top -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) C_ U. J )
3 1 2 sselpwd 
 |-  ( J e. Top -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J )
4 3 adantr 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J )
5 simpl 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> J e. Top )
6 simprl 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> S e. ~P U. J )
7 6 elpwid 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> S C_ U. J )
8 5 7 iscnrm3rlem2 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) )
9 simprr 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> T e. ~P U. J )
10 9 elpwid 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> T C_ U. J )
11 5 10 iscnrm3rlem2 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` T ) i^i ( ( cls ` J ) ` S ) ) ) ) ) )
12 incom 
 |-  ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) = ( ( ( cls ` J ) ` T ) i^i ( ( cls ` J ) ` S ) )
13 12 difeq2i 
 |-  ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) = ( U. J \ ( ( ( cls ` J ) ` T ) i^i ( ( cls ` J ) ` S ) ) )
14 13 oveq2i 
 |-  ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) = ( J |`t ( U. J \ ( ( ( cls ` J ) ` T ) i^i ( ( cls ` J ) ` S ) ) ) )
15 14 fveq2i 
 |-  ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) = ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` T ) i^i ( ( cls ` J ) ` S ) ) ) ) )
16 11 15 eleqtrrdi 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) )
17 4 8 16 3jca 
 |-  ( ( J e. Top /\ ( S e. ~P U. J /\ T e. ~P U. J ) ) -> ( ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) e. ~P U. J /\ ( ( ( cls ` J ) ` S ) \ ( ( cls ` J ) ` T ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) /\ ( ( ( cls ` J ) ` T ) \ ( ( cls ` J ) ` S ) ) e. ( Clsd ` ( J |`t ( U. J \ ( ( ( cls ` J ) ` S ) i^i ( ( cls ` J ) ` T ) ) ) ) ) ) )