Theorem sepcsepo

Description: If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo for the equivalence between separatedness by open neighborhoods and separatedness by neighborhoods. Although J e. Top might be redundant here, it is listed for explicitness. J e. Top can be obtained from neircl , adantr , and rexlimiva . (Contributed by Zhi Wang, 8-Sep-2024)

	Ref	Expression
Hypotheses	sepdisj.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	sepcsepo.2	⊢ ( 𝜑 → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
Assertion	sepcsepo	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		sepcsepo.2	⊢ ( 𝜑 → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
3		simp3	⊢ ( ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ( 𝑛 ∩ 𝑚 ) = ∅ )
4	3	reximi	⊢ ( ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∩ 𝑚 ) = ∅ )
5	4	reximi	⊢ ( ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∩ 𝑚 ) = ∅ )
6	2 5	syl	⊢ ( 𝜑 → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∩ 𝑚 ) = ∅ )
7	1	sepnsepo	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∩ 𝑚 ) = ∅ ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
8	6 7	mpbid	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )