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