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