This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis iscmp.1 
|- X = U. J
Assertion iscmp 
|- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )

Proof

Step Hyp Ref Expression
1 iscmp.1 
 |-  X = U. J
2 pweq 
 |-  ( x = J -> ~P x = ~P J )
3 unieq 
 |-  ( x = J -> U. x = U. J )
4 3 1 eqtr4di 
 |-  ( x = J -> U. x = X )
5 4 eqeq1d 
 |-  ( x = J -> ( U. x = U. y <-> X = U. y ) )
6 4 eqeq1d 
 |-  ( x = J -> ( U. x = U. z <-> X = U. z ) )
7 6 rexbidv 
 |-  ( x = J -> ( E. z e. ( ~P y i^i Fin ) U. x = U. z <-> E. z e. ( ~P y i^i Fin ) X = U. z ) )
8 5 7 imbi12d 
 |-  ( x = J -> ( ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
9 2 8 raleqbidv 
 |-  ( x = J -> ( A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
10 df-cmp 
 |-  Comp = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
11 9 10 elrab2 
 |-  ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )