Theorem dfnrm2

Description: A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm . (Contributed by Zhi Wang, 30-Aug-2024)

	Ref	Expression
Assertion	dfnrm2	|- 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 ) = (/) ) ) }

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	1	abbi2i	|- Nrm = { j | ( 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 ) = (/) ) ) ) }
3		df-rab	|- { 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 ) = (/) ) ) } = { j | ( 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 ) = (/) ) ) ) }
4	2 3	eqtr4i	|- 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 ) = (/) ) ) }