Theorem isnrm4

Description: A topological space is normal iff any two disjoint closed sets are separated by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024)

	Ref	Expression
Assertion	isnrm4	|- ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnrm3	|- ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
2		id	|- ( J e. Top -> J e. Top )
3	2	sepnsepo	|- ( J e. Top -> ( E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) <-> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) )
4	3	imbi2d	|- ( J e. Top -> ( ( ( c i^i d ) = (/) -> E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) ) <-> ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
5	4	2ralbidv	|- ( J e. Top -> ( A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) ) <-> A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
6	5	pm5.32i	|- ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) ) ) <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
7	1 6	bitr4i	|- ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. ( ( nei ` J ) ` c ) E. y e. ( ( nei ` J ) ` d ) ( x i^i y ) = (/) ) ) )