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 ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) 𝐴 = ∪ ran 𝑓 )

Proof

Step Hyp Ref Expression
1 pnrmtop ⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Top )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
4 1 3 sylan ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
5 pnrmcld ⊢ ( ( 𝐽 ∈ PNrm ∧ ( ∪ 𝐽 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 )
6 4 5 syldan ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) → ∃ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 )
7 1 ad2antrr ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) ∧ 𝑥 ∈ ℕ ) → 𝐽 ∈ Top )
8 elmapi ⊢ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) → 𝑔 : ℕ ⟶ 𝐽 )
9 8 adantl ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → 𝑔 : ℕ ⟶ 𝐽 )
10 9 ffvelrnda ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝐽 )
11 2 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
12 7 10 11 syl2anc ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) ∧ 𝑥 ∈ ℕ ) → ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
13 12 fmpttd ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
14 fvex ⊢ ( Clsd ‘ 𝐽 ) ∈ V
15 nnex ⊢ ℕ ∈ V
16 14 15 elmap ⊢ ( ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ↔ ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
17 13 16 sylibr ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) )
18 iundif2 ⊢ ∪ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) = ( ∪ 𝐽 ∖ ∩ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) )
19 ffn ⊢ ( 𝑔 : ℕ ⟶ 𝐽 → 𝑔 Fn ℕ )
20 fniinfv ⊢ ( 𝑔 Fn ℕ → ∩ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∩ ran 𝑔 )
21 9 19 20 3syl ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∩ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∩ ran 𝑔 )
22 21 difeq2d ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ( ∪ 𝐽 ∖ ∩ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) ) = ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) )
23 18 22 syl5eq ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∪ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) = ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) )
24 uniexg ⊢ ( 𝐽 ∈ PNrm → ∪ 𝐽 ∈ V )
25 24 difexd ⊢ ( 𝐽 ∈ PNrm → ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ V )
26 25 ralrimivw ⊢ ( 𝐽 ∈ PNrm → ∀ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ V )
27 26 adantr ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∀ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ V )
28 dfiun2g ⊢ ( ∀ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ∈ V → ∪ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ ℕ 𝑓 = ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) } )
29 27 28 syl ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∪ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ ℕ 𝑓 = ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) } )
30 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) )
31 30 rnmpt ⊢ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) = { 𝑓 ∣ ∃ 𝑥 ∈ ℕ 𝑓 = ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) }
32 31 unieqi ⊢ ∪ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ ℕ 𝑓 = ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) }
33 29 32 eqtr4di ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∪ 𝑥 ∈ ℕ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) = ∪ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) )
34 23 33 eqtr3d ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) )
35 rneq ⊢ ( 𝑓 = ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) → ran 𝑓 = ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) )
36 35 unieqd ⊢ ( 𝑓 = ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) → ∪ ran 𝑓 = ∪ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) )
37 36 rspceeqv ⊢ ( ( ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran ( 𝑥 ∈ ℕ ↦ ( ∪ 𝐽 ∖ ( 𝑔 ‘ 𝑥 ) ) ) ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran 𝑓 )
38 17 34 37 syl2anc ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝑔 ∈ ( 𝐽 ↑m ℕ ) ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran 𝑓 )
39 38 ad2ant2r ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran 𝑓 )
40 difeq2 ⊢ ( ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐴 ) ) = ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) )
41 40 eqcomd ⊢ ( ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 → ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐴 ) ) )
42 elssuni ⊢ ( 𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽 )
43 dfss4 ⊢ ( 𝐴 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐴 ) ) = 𝐴 )
44 42 43 sylib ⊢ ( 𝐴 ∈ 𝐽 → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐴 ) ) = 𝐴 )
45 41 44 sylan9eqr ⊢ ( ( 𝐴 ∈ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) → ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = 𝐴 )
46 45 ad2ant2l ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) ) → ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = 𝐴 )
47 46 eqeq1d ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) ) → ( ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran 𝑓 ↔ 𝐴 = ∪ ran 𝑓 ) )
48 47 rexbidv ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) ) → ( ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) ( ∪ 𝐽 ∖ ∩ ran 𝑔 ) = ∪ ran 𝑓 ↔ ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) 𝐴 = ∪ ran 𝑓 ) )
49 39 48 mpbid ⊢ ( ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑔 ∈ ( 𝐽 ↑m ℕ ) ∧ ( ∪ 𝐽 ∖ 𝐴 ) = ∩ ran 𝑔 ) ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) 𝐴 = ∪ ran 𝑓 )
50 6 49 rexlimddv ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽 ) → ∃ 𝑓 ∈ ( ( Clsd ‘ 𝐽 ) ↑m ℕ ) 𝐴 = ∪ ran 𝑓 )