Theorem dfnrm3

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

	Ref	Expression
Assertion	dfnrm3	|- 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		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 ) = (/) ) ) )
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. ( ( nei ` j ) ` c ) E. y e. ( ( nei ` j ) ` d ) ( 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. ( ( nei ` j ) ` c ) E. y e. ( ( nei ` j ) ` d ) ( 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. ( ( nei ` j ) ` c ) E. y e. ( ( nei ` j ) ` d ) ( 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. ( ( nei ` j ) ` c ) E. y e. ( ( nei ` j ) ` d ) ( x i^i y ) = (/) ) }