ispnrm

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

		Ref	Expression
	Assertion	ispnrm	$⊢ J \in PNrm \leftrightarrow (J \in Nrm \land Clsd (J) \subseteq ran (f \in (J^{ℕ}) ⟼ ⋂ ran f))$

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

Metamath Proof Explorer