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 e. PNrm /\ A e. J ) -> E. f e. ( ( Clsd ` J ) ^m NN ) A = U. ran f )

Proof

Step Hyp Ref Expression
1 pnrmtop 
 |-  ( J e. PNrm -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 opncld 
 |-  ( ( J e. Top /\ A e. J ) -> ( U. J \ A ) e. ( Clsd ` J ) )
4 1 3 sylan 
 |-  ( ( J e. PNrm /\ A e. J ) -> ( U. J \ A ) e. ( Clsd ` J ) )
5 pnrmcld 
 |-  ( ( J e. PNrm /\ ( U. J \ A ) e. ( Clsd ` J ) ) -> E. g e. ( J ^m NN ) ( U. J \ A ) = |^| ran g )
6 4 5 syldan 
 |-  ( ( J e. PNrm /\ A e. J ) -> E. g e. ( J ^m NN ) ( U. J \ A ) = |^| ran g )
7 1 ad2antrr 
 |-  ( ( ( J e. PNrm /\ g e. ( J ^m NN ) ) /\ x e. NN ) -> J e. Top )
8 elmapi 
 |-  ( g e. ( J ^m NN ) -> g : NN --> J )
9 8 adantl 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> g : NN --> J )
10 9 ffvelrnda 
 |-  ( ( ( J e. PNrm /\ g e. ( J ^m NN ) ) /\ x e. NN ) -> ( g ` x ) e. J )
11 2 opncld 
 |-  ( ( J e. Top /\ ( g ` x ) e. J ) -> ( U. J \ ( g ` x ) ) e. ( Clsd ` J ) )
12 7 10 11 syl2anc 
 |-  ( ( ( J e. PNrm /\ g e. ( J ^m NN ) ) /\ x e. NN ) -> ( U. J \ ( g ` x ) ) e. ( Clsd ` J ) )
13 12 fmpttd 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> ( x e. NN |-> ( U. J \ ( g ` x ) ) ) : NN --> ( Clsd ` J ) )
14 fvex 
 |-  ( Clsd ` J ) e. _V
15 nnex 
 |-  NN e. _V
16 14 15 elmap 
 |-  ( ( x e. NN |-> ( U. J \ ( g ` x ) ) ) e. ( ( Clsd ` J ) ^m NN ) <-> ( x e. NN |-> ( U. J \ ( g ` x ) ) ) : NN --> ( Clsd ` J ) )
17 13 16 sylibr 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> ( x e. NN |-> ( U. J \ ( g ` x ) ) ) e. ( ( Clsd ` J ) ^m NN ) )
18 iundif2 
 |-  U_ x e. NN ( U. J \ ( g ` x ) ) = ( U. J \ |^|_ x e. NN ( g ` x ) )
19 ffn 
 |-  ( g : NN --> J -> g Fn NN )
20 fniinfv 
 |-  ( g Fn NN -> |^|_ x e. NN ( g ` x ) = |^| ran g )
21 9 19 20 3syl 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> |^|_ x e. NN ( g ` x ) = |^| ran g )
22 21 difeq2d 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> ( U. J \ |^|_ x e. NN ( g ` x ) ) = ( U. J \ |^| ran g ) )
23 18 22 syl5eq 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> U_ x e. NN ( U. J \ ( g ` x ) ) = ( U. J \ |^| ran g ) )
24 uniexg 
 |-  ( J e. PNrm -> U. J e. _V )
25 24 difexd 
 |-  ( J e. PNrm -> ( U. J \ ( g ` x ) ) e. _V )
26 25 ralrimivw 
 |-  ( J e. PNrm -> A. x e. NN ( U. J \ ( g ` x ) ) e. _V )
27 26 adantr 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> A. x e. NN ( U. J \ ( g ` x ) ) e. _V )
28 dfiun2g 
 |-  ( A. x e. NN ( U. J \ ( g ` x ) ) e. _V -> U_ x e. NN ( U. J \ ( g ` x ) ) = U. { f | E. x e. NN f = ( U. J \ ( g ` x ) ) } )
29 27 28 syl 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> U_ x e. NN ( U. J \ ( g ` x ) ) = U. { f | E. x e. NN f = ( U. J \ ( g ` x ) ) } )
30 eqid 
 |-  ( x e. NN |-> ( U. J \ ( g ` x ) ) ) = ( x e. NN |-> ( U. J \ ( g ` x ) ) )
31 30 rnmpt 
 |-  ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) = { f | E. x e. NN f = ( U. J \ ( g ` x ) ) }
32 31 unieqi 
 |-  U. ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) = U. { f | E. x e. NN f = ( U. J \ ( g ` x ) ) }
33 29 32 eqtr4di 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> U_ x e. NN ( U. J \ ( g ` x ) ) = U. ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) )
34 23 33 eqtr3d 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> ( U. J \ |^| ran g ) = U. ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) )
35 rneq 
 |-  ( f = ( x e. NN |-> ( U. J \ ( g ` x ) ) ) -> ran f = ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) )
36 35 unieqd 
 |-  ( f = ( x e. NN |-> ( U. J \ ( g ` x ) ) ) -> U. ran f = U. ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) )
37 36 rspceeqv 
 |-  ( ( ( x e. NN |-> ( U. J \ ( g ` x ) ) ) e. ( ( Clsd ` J ) ^m NN ) /\ ( U. J \ |^| ran g ) = U. ran ( x e. NN |-> ( U. J \ ( g ` x ) ) ) ) -> E. f e. ( ( Clsd ` J ) ^m NN ) ( U. J \ |^| ran g ) = U. ran f )
38 17 34 37 syl2anc 
 |-  ( ( J e. PNrm /\ g e. ( J ^m NN ) ) -> E. f e. ( ( Clsd ` J ) ^m NN ) ( U. J \ |^| ran g ) = U. ran f )
39 38 ad2ant2r 
 |-  ( ( ( J e. PNrm /\ A e. J ) /\ ( g e. ( J ^m NN ) /\ ( U. J \ A ) = |^| ran g ) ) -> E. f e. ( ( Clsd ` J ) ^m NN ) ( U. J \ |^| ran g ) = U. ran f )
40 difeq2 
 |-  ( ( U. J \ A ) = |^| ran g -> ( U. J \ ( U. J \ A ) ) = ( U. J \ |^| ran g ) )
41 40 eqcomd 
 |-  ( ( U. J \ A ) = |^| ran g -> ( U. J \ |^| ran g ) = ( U. J \ ( U. J \ A ) ) )
42 elssuni 
 |-  ( A e. J -> A C_ U. J )
43 dfss4 
 |-  ( A C_ U. J <-> ( U. J \ ( U. J \ A ) ) = A )
44 42 43 sylib 
 |-  ( A e. J -> ( U. J \ ( U. J \ A ) ) = A )
45 41 44 sylan9eqr 
 |-  ( ( A e. J /\ ( U. J \ A ) = |^| ran g ) -> ( U. J \ |^| ran g ) = A )
46 45 ad2ant2l 
 |-  ( ( ( J e. PNrm /\ A e. J ) /\ ( g e. ( J ^m NN ) /\ ( U. J \ A ) = |^| ran g ) ) -> ( U. J \ |^| ran g ) = A )
47 46 eqeq1d 
 |-  ( ( ( J e. PNrm /\ A e. J ) /\ ( g e. ( J ^m NN ) /\ ( U. J \ A ) = |^| ran g ) ) -> ( ( U. J \ |^| ran g ) = U. ran f <-> A = U. ran f ) )
48 47 rexbidv 
 |-  ( ( ( J e. PNrm /\ A e. J ) /\ ( g e. ( J ^m NN ) /\ ( U. J \ A ) = |^| ran g ) ) -> ( E. f e. ( ( Clsd ` J ) ^m NN ) ( U. J \ |^| ran g ) = U. ran f <-> E. f e. ( ( Clsd ` J ) ^m NN ) A = U. ran f ) )
49 39 48 mpbid 
 |-  ( ( ( J e. PNrm /\ A e. J ) /\ ( g e. ( J ^m NN ) /\ ( U. J \ A ) = |^| ran g ) ) -> E. f e. ( ( Clsd ` J ) ^m NN ) A = U. ran f )
50 6 49 rexlimddv 
 |-  ( ( J e. PNrm /\ A e. J ) -> E. f e. ( ( Clsd ` J ) ^m NN ) A = U. ran f )