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

Theorem iscmp 20345
 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
Assertion
Ref Expression
iscmp
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem iscmp
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pweq 3927 . . 3
2 unieq 4170 . . . . . 6
3 iscmp.1 . . . . . 6
42, 3syl6eqr 2480 . . . . 5
54eqeq1d 2430 . . . 4
64eqeq1d 2430 . . . . 5
76rexbidv 2878 . . . 4
85, 7imbi12d 321 . . 3
91, 8raleqbidv 2978 . 2
10 df-cmp 20344 . 2
119, 10elrab2 3173 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1872  wral 2714  wrex 2715   cin 3378  cpw 3924  cuni 4162  cfn 7524  ctop 19859  ccmp 20343 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-in 3386  df-ss 3393  df-pw 3926  df-uni 4163  df-cmp 20344 This theorem is referenced by:  cmpcov  20346  cncmp  20349  fincmp  20350  cmptop  20352  cmpsub  20357  tgcmp  20358  uncmp  20360  sscmp  20362  cmpfi  20365  comppfsc  20489  txcmp  20600  alexsubb  21003  alexsubALT  21008  cmpcref  28629  onsucsuccmpi  31052  limsucncmpi  31054  heibor  32060
 Copyright terms: Public domain W3C validator