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 incom ⊢ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) )
26 disjdif ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ) = ∅
27 25 26 eqtri ⊢ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) = ∅
28 sseq0 ⊢ ( ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) ⊆ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ )
29 24 27 28 sylancl ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ )
30 sseq2 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( 𝐶 ⊆ 𝑥 ↔ 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ) )
31 ineq1 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) )
32 31 eqeq1d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) )
33 30 32 3anbi13d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) → ( ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) ) )
34 33 rspcev ⊢ ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∈ 𝐽 ∧ ( 𝐶 ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ∧ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ) ∩ 𝑦 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
35 10 19 20 29 34 syl13anc ⊢ ( ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
36 simpl ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐽 ∈ Reg )
37 simpr1 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
38 1 cldopn ⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 )
39 37 38 syl ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 )
40 simpr2 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐴 ∈ 𝑋 )
41 simpr3 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ¬ 𝐴 ∈ 𝐶 )
42 40 41 eldifd ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐴 ∈ ( 𝑋 ∖ 𝐶 ) )
43 regsep ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝑋 ∖ 𝐶 ) ∈ 𝐽 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) )
44 36 39 42 43 syl3anc ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐶 ) ) )
45 35 44 reximddv ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐽 ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
46 rexcom ⊢ ( ∃ 𝑦 ∈ 𝐽 ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
47 45 46 sylib ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )