Step |
Hyp |
Ref |
Expression |
1 |
|
mrccls.f |
|- F = ( mrCls ` ( Clsd ` J ) ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
2
|
clsfval |
|- ( J e. Top -> ( cls ` J ) = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) ) |
4 |
2
|
cldmre |
|- ( J e. Top -> ( Clsd ` J ) e. ( Moore ` U. J ) ) |
5 |
1
|
mrcfval |
|- ( ( Clsd ` J ) e. ( Moore ` U. J ) -> F = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) ) |
6 |
4 5
|
syl |
|- ( J e. Top -> F = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) ) |
7 |
3 6
|
eqtr4d |
|- ( J e. Top -> ( cls ` J ) = F ) |