Theorem iscnrm2

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

	Ref	Expression
Assertion	iscnrm2	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ CNrm ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )

Proof

Step	Hyp	Ref	Expression
1		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	iscnrm	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
4	3	baib	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ CNrm ↔ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
5	1 4	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ CNrm ↔ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
6		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7	6	pweqd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
8	7	raleqdv	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ↔ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
9	5 8	bitr4d	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ CNrm ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )