This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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