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 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐶 ∈ 𝒫 ∪ 𝐽 ∧ 𝐷 ∈ 𝒫 ∪ 𝐽 ) )