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	|- ( ph -> J e. Top )
	sepcsepo.2	|- ( ph -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )
Assertion	sepcsepo	|- ( ph -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	|- ( ph -> J e. Top )
2		sepcsepo.2	|- ( ph -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )
3		simp3	|- ( ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) -> ( n i^i m ) = (/) )
4	3	reximi	|- ( E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) -> E. m e. ( ( nei ` J ) ` T ) ( n i^i m ) = (/) )
5	4	reximi	|- ( E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n i^i m ) = (/) )
6	2 5	syl	|- ( ph -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n i^i m ) = (/) )
7	1	sepnsepo	|- ( ph -> ( E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n i^i m ) = (/) <-> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) )
8	6 7	mpbid	|- ( ph -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) )