Metamath Proof Explorer


Theorem isperf2

Description: Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis lpfval.1
|- X = U. J
Assertion isperf2
|- ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1
 |-  X = U. J
2 1 isperf
 |-  ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )
3 ssid
 |-  X C_ X
4 1 lpss
 |-  ( ( J e. Top /\ X C_ X ) -> ( ( limPt ` J ) ` X ) C_ X )
5 3 4 mpan2
 |-  ( J e. Top -> ( ( limPt ` J ) ` X ) C_ X )
6 eqss
 |-  ( ( ( limPt ` J ) ` X ) = X <-> ( ( ( limPt ` J ) ` X ) C_ X /\ X C_ ( ( limPt ` J ) ` X ) ) )
7 6 baib
 |-  ( ( ( limPt ` J ) ` X ) C_ X -> ( ( ( limPt ` J ) ` X ) = X <-> X C_ ( ( limPt ` J ) ` X ) ) )
8 5 7 syl
 |-  ( J e. Top -> ( ( ( limPt ` J ) ` X ) = X <-> X C_ ( ( limPt ` J ) ` X ) ) )
9 8 pm5.32i
 |-  ( ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )
10 2 9 bitri
 |-  ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )