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