Theorem ispnrm

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

	Ref	Expression
Assertion	ispnrm	$$⊢J\in \mathrm{PNrm}\leftrightarrow \left(J\in \mathrm{Nrm}\wedge \mathrm{Clsd}\left(J\right)\subseteq \mathrm{ran}\left(f\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢j=J\to \mathrm{Clsd}\left(j\right)=\mathrm{Clsd}\left(J\right)$$
2		oveq1	$$⊢j=J\to j^{\mathbb{N}}=J^{\mathbb{N}}$$
3	2	mpteq1d	$$⊢j=J\to \left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)=\left(f\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)$$
4	3	rneqd	$$⊢j=J\to \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)=\mathrm{ran}\left(f\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)$$
5	1 4	sseq12d	$$⊢j=J\to \left(\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\leftrightarrow \mathrm{Clsd}\left(J\right)\subseteq \mathrm{ran}\left(f\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right)$$
6		df-pnrm	$$⊢\mathrm{PNrm}=\left\{j\in \mathrm{Nrm}|\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right\}$$
7	5 6	elrab2	$$⊢J\in \mathrm{PNrm}\leftrightarrow \left(J\in \mathrm{Nrm}\wedge \mathrm{Clsd}\left(J\right)\subseteq \mathrm{ran}\left(f\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right)$$