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 𝑋 = 𝐽
Assertion iscnrm ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽t 𝑥 ) ∈ Nrm ) )

Proof

Step Hyp Ref Expression
1 ist0.1 𝑋 = 𝐽
2 unieq ( 𝑗 = 𝐽 𝑗 = 𝐽 )
3 2 1 eqtr4di ( 𝑗 = 𝐽 𝑗 = 𝑋 )
4 3 pweqd ( 𝑗 = 𝐽 → 𝒫 𝑗 = 𝒫 𝑋 )
5 oveq1 ( 𝑗 = 𝐽 → ( 𝑗t 𝑥 ) = ( 𝐽t 𝑥 ) )
6 5 eleq1d ( 𝑗 = 𝐽 → ( ( 𝑗t 𝑥 ) ∈ Nrm ↔ ( 𝐽t 𝑥 ) ∈ Nrm ) )
7 4 6 raleqbidv ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝒫 𝑗 ( 𝑗t 𝑥 ) ∈ Nrm ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽t 𝑥 ) ∈ Nrm ) )
8 df-cnrm CNrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 𝑗 ( 𝑗t 𝑥 ) ∈ Nrm }
9 7 8 elrab2 ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐽t 𝑥 ) ∈ Nrm ) )