MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscmp Structured version   Unicode version

Theorem iscmp 18891
Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.)
Hypothesis
Ref Expression
iscmp.1  |-  X  = 
U. J
Assertion
Ref Expression
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
) ) )
Distinct variable group:    y, z, J
Allowed substitution hints:    X( y, z)

Proof of Theorem iscmp
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 pweq 3860 . . 3  |-  ( x  =  J  ->  ~P x  =  ~P J
)
2 unieq 4096 . . . . . 6  |-  ( x  =  J  ->  U. x  =  U. J )
3 iscmp.1 . . . . . 6  |-  X  = 
U. J
42, 3syl6eqr 2491 . . . . 5  |-  ( x  =  J  ->  U. x  =  X )
54eqeq1d 2449 . . . 4  |-  ( x  =  J  ->  ( U. x  =  U. y 
<->  X  =  U. y
) )
64eqeq1d 2449 . . . . 5  |-  ( x  =  J  ->  ( U. x  =  U. z 
<->  X  =  U. z
) )
76rexbidv 2734 . . . 4  |-  ( 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 ) )
85, 7imbi12d 320 . . 3  |-  ( 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 ) ) )
91, 8raleqbidv 2929 . 2  |-  ( 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 18890 . 2  |-  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 ) }
119, 10elrab2 3116 1  |-  ( 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
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761   A.wral 2713   E.wrex 2714    i^i cin 3324   ~Pcpw 3857   U.cuni 4088   Fincfn 7306   Topctop 18398   Compccmp 18889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-in 3332  df-ss 3339  df-pw 3859  df-uni 4089  df-cmp 18890
This theorem is referenced by:  cmpcov  18892  cncmp  18895  fincmp  18896  cmptop  18898  cmpsub  18903  tgcmp  18904  uncmp  18906  sscmp  18908  cmpfi  18911  bwthOLD  18914  txcmp  19116  alexsubb  19518  alexsubALT  19523  onsucsuccmpi  28203  limsucncmpi  28205  comppfsc  28488  heibor  28629
  Copyright terms: Public domain W3C validator