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 𝑓 ) ) )