iscnrm3r

Description: Lemma for iscnrm3 . If all subspaces of a topology are normal, i.e., two disjoint closed sets can be separated by open neighborhoods, then in the original topology two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

		Ref	Expression
	Assertion	iscnrm3r	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \to ((S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset) \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset))))$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to J ↾_{𝑡} z = J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))$
2	1	fveq2d	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to Clsd (J ↾_{𝑡} z) = Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))$
3	1	rexeqdv	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to (\exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset) \leftrightarrow \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset))$
4	1 3	rexeqbidv	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to (\exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset) \leftrightarrow \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset))$
5	4	imbi2d	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to ((c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
6	2 5	raleqbidv	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to (\forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
7	2 6	raleqbidv	$⊢ z = ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \to (\forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow \forall c \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
8	7	rspcv	$⊢ ⋃ J ∖ (cls (J) (S) \cap cls (J) (T)) \in 𝒫 ⋃ J \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to \forall c \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
9	8	3ad2ant1	$⊢ (⋃ 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))))) \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to \forall c \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
10		ineq12	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to c \cap d = (cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S))$
11	10	eqeq1d	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to (c \cap d = \emptyset \leftrightarrow (cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset)$
12		simpl	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to c = cls (J) (S) ∖ cls (J) (T)$
13	12	sseq1d	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to (c \subseteq l \leftrightarrow cls (J) (S) ∖ cls (J) (T) \subseteq l)$
14		simpr	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to d = cls (J) (T) ∖ cls (J) (S)$
15	14	sseq1d	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to (d \subseteq k \leftrightarrow cls (J) (T) ∖ cls (J) (S) \subseteq k)$
16	13 15	3anbi12d	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to ((c \subseteq l \land d \subseteq k \land l \cap k = \emptyset) \leftrightarrow (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset))$
17	16	2rexbidv	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to (\exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset) \leftrightarrow \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset))$
18	11 17	imbi12d	$⊢ (c = cls (J) (S) ∖ cls (J) (T) \land d = cls (J) (T) ∖ cls (J) (S)) \to ((c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow ((cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)))$
19	18	rspc2gv	$⊢ (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))))) \to (\forall c \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)))$
20	19	3adant1	$⊢ (⋃ 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))))) \to (\forall c \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \forall d \in Clsd (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)))$
21	9 20	syld	$⊢ (⋃ 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))))) \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)))$
22		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)))))$
23	22	3adant3	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \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)))))$
24		disjdifb	$⊢ (cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset$
25	24	a1i	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \to (cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset$
26		iscnrm3rlem8	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \to (\exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset) \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset))$
27	25 26	embantd	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \to (((cls (J) (S) ∖ cls (J) (T)) \cap (cls (J) (T) ∖ cls (J) (S)) = \emptyset \to \exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset))$
28	21 23 27	iscnrm3lem4	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \to ((S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset) \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset))))$

Metamath Proof Explorer

Theorem iscnrm3r

Proof