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