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 ffvelrnda ⊢ 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 syl5eq ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ⋃ x ∈ ℕ ⋃ J ∖ g ⁡ x = ⋃ J ∖ ⋂ ran ⁡ g
24 uniexg ⊢ J ∈ PNrm → ⋃ J ∈ V
25 difexg ⊢ ⋃ J ∈ V → ⋃ J ∖ g ⁡ x ∈ V
26 24 25 syl ⊢ J ∈ PNrm → ⋃ J ∖ g ⁡ x ∈ V
27 26 ralrimivw ⊢ J ∈ PNrm → ∀ x ∈ ℕ ⋃ J ∖ g ⁡ x ∈ V
28 27 adantr ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ∀ x ∈ ℕ ⋃ J ∖ g ⁡ x ∈ V
29 dfiun2g ⊢ ∀ x ∈ ℕ ⋃ J ∖ g ⁡ x ∈ V → ⋃ x ∈ ℕ ⋃ J ∖ g ⁡ x = ⋃ f | ∃ x ∈ ℕ f = ⋃ J ∖ g ⁡ x
30 28 29 syl ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ⋃ x ∈ ℕ ⋃ J ∖ g ⁡ x = ⋃ f | ∃ x ∈ ℕ f = ⋃ J ∖ g ⁡ x
31 eqid ⊢ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x = x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x
32 31 rnmpt ⊢ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x = f | ∃ x ∈ ℕ f = ⋃ J ∖ g ⁡ x
33 32 unieqi ⊢ ⋃ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x = ⋃ f | ∃ x ∈ ℕ f = ⋃ J ∖ g ⁡ x
34 30 33 eqtr4di ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ⋃ x ∈ ℕ ⋃ J ∖ g ⁡ x = ⋃ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x
35 23 34 eqtr3d ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x
36 rneq ⊢ f = x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x → ran ⁡ f = ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x
37 36 unieqd ⊢ f = x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x → ⋃ ran ⁡ f = ⋃ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x
38 37 rspceeqv ⊢ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x ∈ Clsd ⁡ J ℕ ∧ ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ x ∈ ℕ ⟼ ⋃ J ∖ g ⁡ x → ∃ f ∈ Clsd ⁡ J ℕ ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ f
39 17 35 38 syl2anc ⊢ J ∈ PNrm ∧ g ∈ J ℕ → ∃ f ∈ Clsd ⁡ J ℕ ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ f
40 39 ad2ant2r ⊢ J ∈ PNrm ∧ A ∈ J ∧ g ∈ J ℕ ∧ ⋃ J ∖ A = ⋂ ran ⁡ g → ∃ f ∈ Clsd ⁡ J ℕ ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ f
41 difeq2 ⊢ ⋃ J ∖ A = ⋂ ran ⁡ g → ⋃ J ∖ ⋃ J ∖ A = ⋃ J ∖ ⋂ ran ⁡ g
42 41 eqcomd ⊢ ⋃ J ∖ A = ⋂ ran ⁡ g → ⋃ J ∖ ⋂ ran ⁡ g = ⋃ J ∖ ⋃ J ∖ A
43 elssuni ⊢ A ∈ J → A ⊆ ⋃ J
44 dfss4 ⊢ A ⊆ ⋃ J ↔ ⋃ J ∖ ⋃ J ∖ A = A
45 43 44 sylib ⊢ A ∈ J → ⋃ J ∖ ⋃ J ∖ A = A
46 42 45 sylan9eqr ⊢ A ∈ J ∧ ⋃ J ∖ A = ⋂ ran ⁡ g → ⋃ J ∖ ⋂ ran ⁡ g = A
47 46 ad2ant2l ⊢ J ∈ PNrm ∧ A ∈ J ∧ g ∈ J ℕ ∧ ⋃ J ∖ A = ⋂ ran ⁡ g → ⋃ J ∖ ⋂ ran ⁡ g = A
48 47 eqeq1d ⊢ J ∈ PNrm ∧ A ∈ J ∧ g ∈ J ℕ ∧ ⋃ J ∖ A = ⋂ ran ⁡ g → ⋃ J ∖ ⋂ ran ⁡ g = ⋃ ran ⁡ f ↔ A = ⋃ ran ⁡ f
49 48 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
50 40 49 mpbid ⊢ J ∈ PNrm ∧ A ∈ J ∧ g ∈ J ℕ ∧ ⋃ J ∖ A = ⋂ ran ⁡ g → ∃ f ∈ Clsd ⁡ J ℕ A = ⋃ ran ⁡ f
51 6 50 rexlimddv ⊢ J ∈ PNrm ∧ A ∈ J → ∃ f ∈ Clsd ⁡ J ℕ A = ⋃ ran ⁡ f