Metamath Proof Explorer

Theorem 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 ∈ PNrm ∧ A ∈ J → ∃ f ∈ Clsd ⁡ J ℕ A = ⋃ ran ⁡ f

Proof

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