Metamath Proof Explorer

Theorem iscnrm3llem1

Description: Lemma for iscnrm3l . Closed sets in the subspace are subsets of the underlying set of the original topology. (Contributed by Zhi Wang, 4-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 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 )
3 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 )
4 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 )
5 4 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 )
6 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 ) )
7 2 3 5 6 1 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 ) = (/) ) -> C C_ Z )
8 7 5 sstrd 
 |-  ( ( 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 C_ U. J )
9 1 8 elpwd 
 |-  ( ( 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 )
10 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 ) ) )
11 2 3 5 6 10 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 ) = (/) ) -> D C_ Z )
12 11 5 sstrd 
 |-  ( ( 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 C_ U. J )
13 10 12 elpwd 
 |-  ( ( 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. ~P U. J )
14 9 13 jca 
 |-  ( ( 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 ) )