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∈𝒫XJ↾𝑡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∈𝒫⋃JJ↾𝑡x∈Nrm
4 3 baib ⊢J∈Top→J∈CNrm↔∀x∈𝒫⋃JJ↾𝑡x∈Nrm
5 1 4 syl ⊢J∈TopOn⁡X→J∈CNrm↔∀x∈𝒫⋃JJ↾𝑡x∈Nrm
6 toponuni ⊢J∈TopOn⁡X→X=⋃J
7 6 pweqd ⊢J∈TopOn⁡X→𝒫X=𝒫⋃J
8 7 raleqdv ⊢J∈TopOn⁡X→∀x∈𝒫XJ↾𝑡x∈Nrm↔∀x∈𝒫⋃JJ↾𝑡x∈Nrm
9 5 8 bitr4d ⊢J∈TopOn⁡X→J∈CNrm↔∀x∈𝒫XJ↾𝑡x∈Nrm