Description: Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mrccls.f | ⊢ 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) | |
Assertion | mrccls | ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrccls.f | ⊢ 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) | |
2 | eqid | ⊢ ∪ 𝐽 = ∪ 𝐽 | |
3 | 2 | clsfval | ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) ) |
4 | 2 | cldmre | ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) ) |
5 | 1 | mrcfval | ⊢ ( ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) → 𝐹 = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) ) |
6 | 4 5 | syl | ⊢ ( 𝐽 ∈ Top → 𝐹 = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) ) |
7 | 3 6 | eqtr4d | ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 ) |