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 𝑋 = 𝐽
Assertion hausmapdom ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴m ℕ ) )

Proof

Step Hyp Ref Expression
1 hauspwdom.1 𝑋 = 𝐽
2 1 1stcelcls ( ( 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ) )
3 2 3adant1 ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ) )
4 uniexg ( 𝐽 ∈ Haus → 𝐽 ∈ V )
5 4 3ad2ant1 ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → 𝐽 ∈ V )
6 1 5 eqeltrid ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → 𝑋 ∈ V )
7 simp3 ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → 𝐴𝑋 )
8 6 7 ssexd ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → 𝐴 ∈ V )
9 nnex ℕ ∈ V
10 elmapg ( ( 𝐴 ∈ V ∧ ℕ ∈ V ) → ( 𝑓 ∈ ( 𝐴m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐴 ) )
11 8 9 10 sylancl ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑓 ∈ ( 𝐴m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐴 ) )
12 11 anbi1d ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ( 𝑓 ∈ ( 𝐴m ℕ ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ↔ ( 𝑓 : ℕ ⟶ 𝐴𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ) )
13 12 exbidv ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ∃ 𝑓 ( 𝑓 ∈ ( 𝐴m ℕ ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ) )
14 3 13 bitr4d ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐴m ℕ ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) ) )
15 df-rex ( ∃ 𝑓 ∈ ( 𝐴m ℕ ) 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐴m ℕ ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) )
16 14 15 bitr4di ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ∈ ( 𝐴m ℕ ) 𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) )
17 vex 𝑥 ∈ V
18 17 elima ( 𝑥 ∈ ( ( ⇝𝑡𝐽 ) “ ( 𝐴m ℕ ) ) ↔ ∃ 𝑓 ∈ ( 𝐴m ℕ ) 𝑓 ( ⇝𝑡𝐽 ) 𝑥 )
19 16 18 bitr4di ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ ( ( ⇝𝑡𝐽 ) “ ( 𝐴m ℕ ) ) ) )
20 19 eqrdv ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( ⇝𝑡𝐽 ) “ ( 𝐴m ℕ ) ) )
21 ovex ( 𝐴m ℕ ) ∈ V
22 lmfun ( 𝐽 ∈ Haus → Fun ( ⇝𝑡𝐽 ) )
23 22 3ad2ant1 ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → Fun ( ⇝𝑡𝐽 ) )
24 imadomg ( ( 𝐴m ℕ ) ∈ V → ( Fun ( ⇝𝑡𝐽 ) → ( ( ⇝𝑡𝐽 ) “ ( 𝐴m ℕ ) ) ≼ ( 𝐴m ℕ ) ) )
25 21 23 24 mpsyl ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ( ⇝𝑡𝐽 ) “ ( 𝐴m ℕ ) ) ≼ ( 𝐴m ℕ ) )
26 20 25 eqbrtrd ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴m ℕ ) )