This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℕ ) )