Metamath Proof Explorer


Theorem isperf

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

Proof

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