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

Metamath Proof Explorer

Theorem ispnrm

Description: The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ispnrm ( 𝐽 ∈ PNrm ↔ ( 𝐽 ∈ Nrm ∧ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑗 = 𝐽 → ( Clsd ‘ 𝑗 ) = ( Clsd ‘ 𝐽 ) )
2 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ↑m ℕ ) = ( 𝐽 ↑m ℕ ) )
3 2 mpteq1d ⊢ ( 𝑗 = 𝐽 → ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) = ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) )
4 3 rneqd ⊢ ( 𝑗 = 𝐽 → ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) = ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) )
5 1 4 sseq12d ⊢ ( 𝑗 = 𝐽 → ( ( Clsd ‘ 𝑗 ) ⊆ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ↔ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ) )
6 df-pnrm ⊢ PNrm = { 𝑗 ∈ Nrm ∣ ( Clsd ‘ 𝑗 ) ⊆ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) }
7 5 6 elrab2 ⊢ ( 𝐽 ∈ PNrm ↔ ( 𝐽 ∈ Nrm ∧ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ) )