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 ‘ 𝐽 ) )