Metamath Proof Explorer


Theorem hauscmp

Description: A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010) (Proof shortened by Mario Carneiro, 14-Dec-2013)

Ref Expression
Hypothesis hauscmp.1 𝑋 = 𝐽
Assertion hauscmp ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 hauscmp.1 𝑋 = 𝐽
2 simp2 ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → 𝑆𝑋 )
3 eqid { 𝑦𝐽 ∣ ∃ 𝑤𝐽 ( 𝑥𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋𝑦 ) ) } = { 𝑦𝐽 ∣ ∃ 𝑤𝐽 ( 𝑥𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋𝑦 ) ) }
4 simpl1 ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → 𝐽 ∈ Haus )
5 simpl2 ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → 𝑆𝑋 )
6 simpl3 ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → ( 𝐽t 𝑆 ) ∈ Comp )
7 simpr ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → 𝑥 ∈ ( 𝑋𝑆 ) )
8 1 3 4 5 6 7 hauscmplem ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → ∃ 𝑧𝐽 ( 𝑥𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) ) )
9 haustop ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
10 9 3ad2ant1 ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → 𝐽 ∈ Top )
11 elssuni ( 𝑧𝐽𝑧 𝐽 )
12 11 1 sseqtrrdi ( 𝑧𝐽𝑧𝑋 )
13 1 sscls ( ( 𝐽 ∈ Top ∧ 𝑧𝑋 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
14 10 12 13 syl2an ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑧𝐽 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
15 sstr2 ( 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) → 𝑧 ⊆ ( 𝑋𝑆 ) ) )
16 14 15 syl ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑧𝐽 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) → 𝑧 ⊆ ( 𝑋𝑆 ) ) )
17 16 anim2d ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑧𝐽 ) → ( ( 𝑥𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) ) → ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) ) )
18 17 reximdva ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → ( ∃ 𝑧𝐽 ( 𝑥𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) ) → ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) ) )
19 18 adantr ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → ( ∃ 𝑧𝐽 ( 𝑥𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋𝑆 ) ) → ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) ) )
20 8 19 mpd ( ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋𝑆 ) ) → ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) )
21 20 ralrimiva ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → ∀ 𝑥 ∈ ( 𝑋𝑆 ) ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) )
22 eltop2 ( 𝐽 ∈ Top → ( ( 𝑋𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝑋𝑆 ) ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) ) )
23 10 22 syl ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → ( ( 𝑋𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝑋𝑆 ) ∃ 𝑧𝐽 ( 𝑥𝑧𝑧 ⊆ ( 𝑋𝑆 ) ) ) )
24 21 23 mpbird ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → ( 𝑋𝑆 ) ∈ 𝐽 )
25 1 iscld ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆𝑋 ∧ ( 𝑋𝑆 ) ∈ 𝐽 ) ) )
26 10 25 syl ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆𝑋 ∧ ( 𝑋𝑆 ) ∈ 𝐽 ) ) )
27 2 24 26 mpbir2and ( ( 𝐽 ∈ Haus ∧ 𝑆𝑋 ∧ ( 𝐽t 𝑆 ) ∈ Comp ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )