Metamath Proof Explorer

Theorem 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 ∈ CNrm ↔ J ∈ Top ∧ ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 unieq ⊢ j = J → ⋃ j = ⋃ J
3 2 1 eqtr4di ⊢ j = J → ⋃ j = X
4 3 pweqd ⊢ j = J → 𝒫 ⋃ j = 𝒫 X
5 oveq1 ⊢ j = J → j ↾ 𝑡 x = J ↾ 𝑡 x
6 5 eleq1d ⊢ j = J → j ↾ 𝑡 x ∈ Nrm ↔ J ↾ 𝑡 x ∈ Nrm
7 4 6 raleqbidv ⊢ j = J → ∀ x ∈ 𝒫 ⋃ j j ↾ 𝑡 x ∈ Nrm ↔ ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm
8 df-cnrm ⊢ CNrm = j ∈ Top | ∀ x ∈ 𝒫 ⋃ j j ↾ 𝑡 x ∈ Nrm
9 7 8 elrab2 ⊢ J ∈ CNrm ↔ J ∈ Top ∧ ∀ x ∈ 𝒫 X J ↾ 𝑡 x ∈ Nrm