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 \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \in 𝒫 ⋃ J \land cls (J) (S) ∖ cls (J) (T) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land cls (J) (T) ∖ cls (J) (S) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))))$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$⊢ J \in Top \to ⋃ J \in V$
2		difssd	$⊢ J \in Top \to ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \subseteq ⋃ J$
3	1 2	sselpwd	$⊢ J \in Top \to ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \in 𝒫 ⋃ J$
4	3	adantr	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \in 𝒫 ⋃ J$
5		simpl	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to J \in Top$
6		simprl	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to S \in 𝒫 ⋃ J$
7	6	elpwid	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to S \subseteq ⋃ J$
8	5 7	iscnrm3rlem2	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to cls (J) (S) ∖ cls (J) (T) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))$
9		simprr	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to T \in 𝒫 ⋃ J$
10	9	elpwid	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to T \subseteq ⋃ J$
11	5 10	iscnrm3rlem2	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to cls (J) (T) ∖ cls (J) (S) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (T) \cap cls (J) (S))))$
12		incom	$⊢ cls (J) (S) \cap cls (J) (T) = cls (J) (T) \cap cls (J) (S)$
13	12	difeq2i	$⊢ ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) = ⋃ J ∖ (cls (J) (T) \cap cls (J) (S))$
14	13	oveq2i	$⊢ J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))) = J ↾_{𝑡} (⋃ J ∖ (cls (J) (T) \cap cls (J) (S)))$
15	14	fveq2i	$⊢ Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) = Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (T) \cap cls (J) (S))))$
16	11 15	eleqtrrdi	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to cls (J) (T) ∖ cls (J) (S) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))$
17	4 8 16	3jca	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J)) \to (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \in 𝒫 ⋃ J \land cls (J) (S) ∖ cls (J) (T) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land cls (J) (T) ∖ cls (J) (S) \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))))$