pnrmopn

Description: An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	pnrmopn	$⊢ (J \in PNrm \land A \in J) \to \exists f \in ({Clsd (J)}^{ℕ}) A = ⋃ ran f$

Proof

Step	Hyp	Ref	Expression
1		pnrmtop	$⊢ J \in PNrm \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	opncld	$⊢ (J \in Top \land A \in J) \to ⋃ J ∖ A \in Clsd (J)$
4	1 3	sylan	$⊢ (J \in PNrm \land A \in J) \to ⋃ J ∖ A \in Clsd (J)$
5		pnrmcld	$⊢ (J \in PNrm \land ⋃ J ∖ A \in Clsd (J)) \to \exists g \in (J^{ℕ}) ⋃ J ∖ A = ⋂ ran g$
6	4 5	syldan	$⊢ (J \in PNrm \land A \in J) \to \exists g \in (J^{ℕ}) ⋃ J ∖ A = ⋂ ran g$
7	1	ad2antrr	$⊢ ((J \in PNrm \land g \in (J^{ℕ})) \land x \in ℕ) \to J \in Top$
8		elmapi	$⊢ g \in (J^{ℕ}) \to g : ℕ ⟶ J$
9	8	adantl	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to g : ℕ ⟶ J$
10	9	ffvelcdmda	$⊢ ((J \in PNrm \land g \in (J^{ℕ})) \land x \in ℕ) \to g (x) \in J$
11	2	opncld	$⊢ (J \in Top \land g (x) \in J) \to ⋃ J ∖ g (x) \in Clsd (J)$
12	7 10 11	syl2anc	$⊢ ((J \in PNrm \land g \in (J^{ℕ})) \land x \in ℕ) \to ⋃ J ∖ g (x) \in Clsd (J)$
13	12	fmpttd	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to (x \in ℕ ⟼ ⋃ J ∖ g (x)) : ℕ ⟶ Clsd (J)$
14		fvex	$⊢ Clsd (J) \in V$
15		nnex	$⊢ ℕ \in V$
16	14 15	elmap	$⊢ (x \in ℕ ⟼ ⋃ J ∖ g (x)) \in ({Clsd (J)}^{ℕ}) \leftrightarrow (x \in ℕ ⟼ ⋃ J ∖ g (x)) : ℕ ⟶ Clsd (J)$
17	13 16	sylibr	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to (x \in ℕ ⟼ ⋃ J ∖ g (x)) \in ({Clsd (J)}^{ℕ})$
18		iundif2	$⊢ ⋃_{x \in ℕ} (⋃ J ∖ g (x)) = ⋃ J ∖ ⋂_{x \in ℕ} g (x)$
19		ffn	$⊢ g : ℕ ⟶ J \to g Fn ℕ$
20		fniinfv	$⊢ g Fn ℕ \to ⋂_{x \in ℕ} g (x) = ⋂ ran g$
21	9 19 20	3syl	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋂_{x \in ℕ} g (x) = ⋂ ran g$
22	21	difeq2d	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋃ J ∖ ⋂_{x \in ℕ} g (x) = ⋃ J ∖ ⋂ ran g$
23	18 22	eqtrid	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋃_{x \in ℕ} (⋃ J ∖ g (x)) = ⋃ J ∖ ⋂ ran g$
24		uniexg	$⊢ J \in PNrm \to ⋃ J \in V$
25	24	difexd	$⊢ J \in PNrm \to ⋃ J ∖ g (x) \in V$
26	25	ralrimivw	$⊢ J \in PNrm \to \forall x \in ℕ ⋃ J ∖ g (x) \in V$
27	26	adantr	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to \forall x \in ℕ ⋃ J ∖ g (x) \in V$
28		dfiun2g	$⊢ \forall x \in ℕ ⋃ J ∖ g (x) \in V \to ⋃_{x \in ℕ} (⋃ J ∖ g (x)) = ⋃ \{f \| \exists x \in ℕ f = ⋃ J ∖ g (x)\}$
29	27 28	syl	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋃_{x \in ℕ} (⋃ J ∖ g (x)) = ⋃ \{f \| \exists x \in ℕ f = ⋃ J ∖ g (x)\}$
30		eqid	$⊢ (x \in ℕ ⟼ ⋃ J ∖ g (x)) = (x \in ℕ ⟼ ⋃ J ∖ g (x))$
31	30	rnmpt	$⊢ ran (x \in ℕ ⟼ ⋃ J ∖ g (x)) = \{f \| \exists x \in ℕ f = ⋃ J ∖ g (x)\}$
32	31	unieqi	$⊢ ⋃ ran (x \in ℕ ⟼ ⋃ J ∖ g (x)) = ⋃ \{f \| \exists x \in ℕ f = ⋃ J ∖ g (x)\}$
33	29 32	eqtr4di	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋃_{x \in ℕ} (⋃ J ∖ g (x)) = ⋃ ran (x \in ℕ ⟼ ⋃ J ∖ g (x))$
34	23 33	eqtr3d	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to ⋃ J ∖ ⋂ ran g = ⋃ ran (x \in ℕ ⟼ ⋃ J ∖ g (x))$
35		rneq	$⊢ f = (x \in ℕ ⟼ ⋃ J ∖ g (x)) \to ran f = ran (x \in ℕ ⟼ ⋃ J ∖ g (x))$
36	35	unieqd	$⊢ f = (x \in ℕ ⟼ ⋃ J ∖ g (x)) \to ⋃ ran f = ⋃ ran (x \in ℕ ⟼ ⋃ J ∖ g (x))$
37	36	rspceeqv	$⊢ ((x \in ℕ ⟼ ⋃ J ∖ g (x)) \in ({Clsd (J)}^{ℕ}) \land ⋃ J ∖ ⋂ ran g = ⋃ ran (x \in ℕ ⟼ ⋃ J ∖ g (x))) \to \exists f \in ({Clsd (J)}^{ℕ}) ⋃ J ∖ ⋂ ran g = ⋃ ran f$
38	17 34 37	syl2anc	$⊢ (J \in PNrm \land g \in (J^{ℕ})) \to \exists f \in ({Clsd (J)}^{ℕ}) ⋃ J ∖ ⋂ ran g = ⋃ ran f$
39	38	ad2ant2r	$⊢ ((J \in PNrm \land A \in J) \land (g \in (J^{ℕ}) \land ⋃ J ∖ A = ⋂ ran g)) \to \exists f \in ({Clsd (J)}^{ℕ}) ⋃ J ∖ ⋂ ran g = ⋃ ran f$
40		difeq2	$⊢ ⋃ J ∖ A = ⋂ ran g \to ⋃ J ∖ (⋃ J ∖ A) = ⋃ J ∖ ⋂ ran g$
41	40	eqcomd	$⊢ ⋃ J ∖ A = ⋂ ran g \to ⋃ J ∖ ⋂ ran g = ⋃ J ∖ (⋃ J ∖ A)$
42		elssuni	$⊢ A \in J \to A \subseteq ⋃ J$
43		dfss4	$⊢ A \subseteq ⋃ J \leftrightarrow ⋃ J ∖ (⋃ J ∖ A) = A$
44	42 43	sylib	$⊢ A \in J \to ⋃ J ∖ (⋃ J ∖ A) = A$
45	41 44	sylan9eqr	$⊢ (A \in J \land ⋃ J ∖ A = ⋂ ran g) \to ⋃ J ∖ ⋂ ran g = A$
46	45	ad2ant2l	$⊢ ((J \in PNrm \land A \in J) \land (g \in (J^{ℕ}) \land ⋃ J ∖ A = ⋂ ran g)) \to ⋃ J ∖ ⋂ ran g = A$
47	46	eqeq1d	$⊢ ((J \in PNrm \land A \in J) \land (g \in (J^{ℕ}) \land ⋃ J ∖ A = ⋂ ran g)) \to (⋃ J ∖ ⋂ ran g = ⋃ ran f \leftrightarrow A = ⋃ ran f)$
48	47	rexbidv	$⊢ ((J \in PNrm \land A \in J) \land (g \in (J^{ℕ}) \land ⋃ J ∖ A = ⋂ ran g)) \to (\exists f \in ({Clsd (J)}^{ℕ}) ⋃ J ∖ ⋂ ran g = ⋃ ran f \leftrightarrow \exists f \in ({Clsd (J)}^{ℕ}) A = ⋃ ran f)$
49	39 48	mpbid	$⊢ ((J \in PNrm \land A \in J) \land (g \in (J^{ℕ}) \land ⋃ J ∖ A = ⋂ ran g)) \to \exists f \in ({Clsd (J)}^{ℕ}) A = ⋃ ran f$
50	6 49	rexlimddv	$⊢ (J \in PNrm \land A \in J) \to \exists f \in ({Clsd (J)}^{ℕ}) A = ⋃ ran f$

Metamath Proof Explorer

Theorem pnrmopn

Proof