This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )