Description: Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lpfval.1 | |- X = U. J |
|
Assertion | isperf | |- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lpfval.1 | |- X = U. J |
|
2 | fveq2 | |- ( j = J -> ( limPt ` j ) = ( limPt ` J ) ) |
|
3 | unieq | |- ( j = J -> U. j = U. J ) |
|
4 | 3 1 | eqtr4di | |- ( j = J -> U. j = X ) |
5 | 2 4 | fveq12d | |- ( j = J -> ( ( limPt ` j ) ` U. j ) = ( ( limPt ` J ) ` X ) ) |
6 | 5 4 | eqeq12d | |- ( j = J -> ( ( ( limPt ` j ) ` U. j ) = U. j <-> ( ( limPt ` J ) ` X ) = X ) ) |
7 | df-perf | |- Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j } |
|
8 | 6 7 | elrab2 | |- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) ) |