Metamath Proof Explorer

Theorem hausmapdom

Description: If X is a first-countable Hausdorff space, then the cardinality of the closure of a set A is bounded by NN to the power A . In particular, a first-countable Hausdorff space with a dense subset A has cardinality at most A ^ NN , and a separable first-countable Hausdorff space has cardinality at most ~P NN . (Compare hauspwpwdom to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis hauspwdom.1 
|- X = U. J
Assertion hausmapdom 
|- ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ( A ^m NN ) )

Proof

Step Hyp Ref Expression
1 hauspwdom.1 
 |-  X = U. J
2 1 1stcelcls 
 |-  ( ( J e. 1stc /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) <-> E. f ( f : NN --> A /\ f ( ~~>t ` J ) x ) ) )
3 2 3adant1 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) <-> E. f ( f : NN --> A /\ f ( ~~>t ` J ) x ) ) )
4 uniexg 
 |-  ( J e. Haus -> U. J e. _V )
5 4 3ad2ant1 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> U. J e. _V )
6 1 5 eqeltrid 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> X e. _V )
7 simp3 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> A C_ X )
8 6 7 ssexd 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> A e. _V )
9 nnex 
 |-  NN e. _V
10 elmapg 
 |-  ( ( A e. _V /\ NN e. _V ) -> ( f e. ( A ^m NN ) <-> f : NN --> A ) )
11 8 9 10 sylancl 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( f e. ( A ^m NN ) <-> f : NN --> A ) )
12 11 anbi1d 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( f e. ( A ^m NN ) /\ f ( ~~>t ` J ) x ) <-> ( f : NN --> A /\ f ( ~~>t ` J ) x ) ) )
13 12 exbidv 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( E. f ( f e. ( A ^m NN ) /\ f ( ~~>t ` J ) x ) <-> E. f ( f : NN --> A /\ f ( ~~>t ` J ) x ) ) )
14 3 13 bitr4d 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) <-> E. f ( f e. ( A ^m NN ) /\ f ( ~~>t ` J ) x ) ) )
15 df-rex 
 |-  ( E. f e. ( A ^m NN ) f ( ~~>t ` J ) x <-> E. f ( f e. ( A ^m NN ) /\ f ( ~~>t ` J ) x ) )
16 14 15 bitr4di 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) <-> E. f e. ( A ^m NN ) f ( ~~>t ` J ) x ) )
17 vex 
 |-  x e. _V
18 17 elima 
 |-  ( x e. ( ( ~~>t ` J ) " ( A ^m NN ) ) <-> E. f e. ( A ^m NN ) f ( ~~>t ` J ) x )
19 16 18 bitr4di 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) <-> x e. ( ( ~~>t ` J ) " ( A ^m NN ) ) ) )
20 19 eqrdv 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( cls ` J ) ` A ) = ( ( ~~>t ` J ) " ( A ^m NN ) ) )
21 ovex 
 |-  ( A ^m NN ) e. _V
22 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
23 22 3ad2ant1 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> Fun ( ~~>t ` J ) )
24 imadomg 
 |-  ( ( A ^m NN ) e. _V -> ( Fun ( ~~>t ` J ) -> ( ( ~~>t ` J ) " ( A ^m NN ) ) ~<_ ( A ^m NN ) ) )
25 21 23 24 mpsyl 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( ~~>t ` J ) " ( A ^m NN ) ) ~<_ ( A ^m NN ) )
26 20 25 eqbrtrd 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ( A ^m NN ) )