iscnrm

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

		Ref	Expression
	Hypothesis	ist0.1	$⊢ X = ⋃ J$
	Assertion	iscnrm	$⊢ J \in CNrm \leftrightarrow (J \in Top \land \forall x \in 𝒫 X J ↾_{𝑡} x \in Nrm)$

Step	Hyp	Ref	Expression
1		ist0.1	$⊢ X = ⋃ J$
2		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
3	2 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
4	3	pweqd	$⊢ j = J \to 𝒫 ⋃ j = 𝒫 X$
5		oveq1	$⊢ j = J \to j ↾_{𝑡} x = J ↾_{𝑡} x$
6	5	eleq1d	$⊢ j = J \to (j ↾_{𝑡} x \in Nrm \leftrightarrow J ↾_{𝑡} x \in Nrm)$
7	4 6	raleqbidv	$⊢ j = J \to (\forall x \in 𝒫 ⋃ j j ↾_{𝑡} x \in Nrm \leftrightarrow \forall x \in 𝒫 X J ↾_{𝑡} x \in Nrm)$
8		df-cnrm	$⊢ CNrm = \{j \in Top \| \forall x \in 𝒫 ⋃ j j ↾_{𝑡} x \in Nrm\}$
9	7 8	elrab2	$⊢ J \in CNrm \leftrightarrow (J \in Top \land \forall x \in 𝒫 X J ↾_{𝑡} x \in Nrm)$

Metamath Proof Explorer