Metamath Proof Explorer

Theorem regsep2

Description: In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis t1sep.1 ⊢ 𝑋 = ∪ 𝐽
Assertion regsep2 ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ 𝑋 = ∪ 𝐽
2 regtop ⊢ ( 𝐽 ∈ Reg → 𝐽 ∈ Top )
3 2 ad2antrr ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝐽 ∈ Top )
4 elssuni ⊢ ( 𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽 )
5 4 1 sseqtrrdi ⊢ ( 𝑦 ∈ 𝐽 → 𝑦 ⊆ 𝑋 )
6 5 ad2antrl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝑦 ⊆ 𝑋 )
7 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
8 3 6 7 syl2anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
9 1 cldopn ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∈ 𝐽 )
10 8 9 syl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∈ 𝐽 )
11 simprrr ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) )
12 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑋 )
13 3 6 12 syl2anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑋 )
14 simplr1 ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
15 1 cldss ⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐶 ⊆ 𝑋 )
16 14 15 syl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝐶 ⊆ 𝑋 )
17 ssconb ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑋 ∧ 𝐶 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ↔ 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ) )
18 13 16 17 syl2anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ↔ 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ) )
19 11 18 mpbid ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) )
20 simprrl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝐴 ∈ 𝑦 )
21 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝑋 ) → 𝑦 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) )
22 3 6 21 syl2anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → 𝑦 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) )
23 sslin ⊢ ( 𝑦 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) ⊆ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) )
24 22 23 syl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) ⊆ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) )
25 disjdifr ⊢ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) = ∅
26 sseq0 ⊢ ( ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) ⊆ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ )
27 24 25 26 sylancl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ )
28 sseq2 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( 𝐶 ⊆ 𝑥 ↔ 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ) )
29 ineq1 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) )
30 29 eqeq1d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) )
31 28 30 3anbi13d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) ) )
32 31 rspcev ⊢ ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∈ 𝐽 ∧ ( 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
33 10 19 20 27 32 syl13anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
34 simpl ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐽 ∈ Reg )
35 simpr1 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
36 1 cldopn ⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 )
37 35 36 syl ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 )
38 simpr2 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐴 ∈ 𝑋 )
39 simpr3 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ¬ 𝐴 ∈ 𝐶 )
40 38 39 eldifd ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐴 ∈ ( 𝑋 ∖ 𝐶 ) )
41 regsep ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) )
42 34 37 40 41 syl3anc ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) )
43 33 42 reximddv ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
44 rexcom ⊢ ( ∃ 𝑦 ∈ 𝐽 ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
45 43 44 sylib ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )