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 \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (C \in 𝒫 ⋃ J \land D \in 𝒫 ⋃ J)$

Proof

Step	Hyp	Ref	Expression
1		simp22	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \in Clsd (J ↾_{𝑡} Z)$
2		simp1	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to J \in Top$
3		eqidd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to ⋃ J = ⋃ J$
4		simp21	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to Z \in 𝒫 ⋃ J$
5	4	elpwid	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to Z \subseteq ⋃ J$
6		eqidd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to J ↾_{𝑡} Z = J ↾_{𝑡} Z$
7	2 3 5 6 1	restcls2lem	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \subseteq Z$
8	7 5	sstrd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \subseteq ⋃ J$
9	1 8	elpwd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \in 𝒫 ⋃ J$
10		simp23	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to D \in Clsd (J ↾_{𝑡} Z)$
11	2 3 5 6 10	restcls2lem	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to D \subseteq Z$
12	11 5	sstrd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to D \subseteq ⋃ J$
13	10 12	elpwd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to D \in 𝒫 ⋃ J$
14	9 13	jca	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (C \in 𝒫 ⋃ J \land D \in 𝒫 ⋃ J)$