Theorem isnrm

Description: The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Assertion	isnrm	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐽 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑗 = 𝐽 → ( Clsd ‘ 𝑗 ) = ( Clsd ‘ 𝐽 ) )
2	1	ineq1d	⊢ ( 𝑗 = 𝐽 → ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) = ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) )
3		fveq2	⊢ ( 𝑗 = 𝐽 → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) )
4	3	fveq1d	⊢ ( 𝑗 = 𝐽 → ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
5	4	sseq1d	⊢ ( 𝑗 = 𝐽 → ( ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
6	5	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
7	6	rexeqbi1dv	⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐽 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
8	2 7	raleqbidv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐽 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
9	8	raleqbi1dv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐽 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
10		df-nrm	⊢ Nrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }
11	9 10	elrab2	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐽 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )