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 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → ( 𝐶 ∈ 𝒫 𝐽𝐷 ∈ 𝒫 𝐽 ) )

Proof

Step Hyp Ref Expression
1 simp22 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) )
2 simp1 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐽 ∈ Top )
3 eqidd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐽 = 𝐽 )
4 simp21 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝑍 ∈ 𝒫 𝐽 )
5 4 elpwid ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝑍 𝐽 )
6 eqidd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → ( 𝐽t 𝑍 ) = ( 𝐽t 𝑍 ) )
7 2 3 5 6 1 restcls2lem ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐶𝑍 )
8 7 5 sstrd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐶 𝐽 )
9 1 8 elpwd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐶 ∈ 𝒫 𝐽 )
10 simp23 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) )
11 2 3 5 6 10 restcls2lem ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐷𝑍 )
12 11 5 sstrd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐷 𝐽 )
13 10 12 elpwd ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → 𝐷 ∈ 𝒫 𝐽 )
14 9 13 jca ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 𝐽𝐶 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽t 𝑍 ) ) ) ∧ ( 𝐶𝐷 ) = ∅ ) → ( 𝐶 ∈ 𝒫 𝐽𝐷 ∈ 𝒫 𝐽 ) )