Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hausmapdom Unicode version

Theorem hausmapdom 17443
 Description: If is a first-countable Hausdorff space, then the cardinality of the closure of a set is bounded by to the power . In particular, a first-countable Hausdorff space with a dense subset has cardinality at most , and a separable first-countable Hausdorff space has cardinality at most . (Compare hauspwpwdom 17896 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.)
Hypothesis
Ref Expression
hauspwdom.1
Assertion
Ref Expression
hausmapdom

Proof of Theorem hausmapdom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hauspwdom.1 . . . . . . . 8
211stcelcls 17404 . . . . . . 7
323adant1 974 . . . . . 6
4 simp3 958 . . . . . . . . . 10
5 uniexg 4620 . . . . . . . . . . . 12
653ad2ant1 977 . . . . . . . . . . 11
71, 6syl5eqel 2450 . . . . . . . . . 10
8 ssexg 4262 . . . . . . . . . 10
94, 7, 8syl2anc 642 . . . . . . . . 9
10 nnex 9899 . . . . . . . . 9
11 elmapg 6928 . . . . . . . . 9
129, 10, 11sylancl 643 . . . . . . . 8
1312anbi1d 685 . . . . . . 7
1413exbidv 1631 . . . . . 6
153, 14bitr4d 247 . . . . 5
16 df-rex 2634 . . . . 5
1715, 16syl6bbr 254 . . . 4
18 vex 2876 . . . . 5
1918elima 5120 . . . 4
2017, 19syl6bbr 254 . . 3
2120eqrdv 2364 . 2
22 ovex 6006 . . 3
23 lmfun 17326 . . . 4