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 ⊢ J ∈ TopOn ⁡ X → J ∈ CNrm ↔ ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 eqid ⊢ ⋃ J = ⋃ J
3 2 iscnrm ⊢ J ∈ CNrm ↔ J ∈ Top ∧ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
4 3 baib ⊢ J ∈ Top → J ∈ CNrm ↔ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
5 1 4 syl ⊢ J ∈ TopOn ⁡ X → J ∈ CNrm ↔ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
6 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
7 6 pweqd ⊢ J ∈ TopOn ⁡ X → 𝒫 X = 𝒫 ⋃ J
8 7 raleqdv ⊢ J ∈ TopOn ⁡ X → ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm ↔ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
9 5 8 bitr4d ⊢ J ∈ TopOn ⁡ X → J ∈ CNrm ↔ ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm