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

Theorem iscmp 17444
 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 3795 . . 3
2 unieq 4017 . . . . . 6
3 iscmp.1 . . . . . 6
42, 3syl6eqr 2486 . . . . 5
54eqeq1d 2444 . . . 4
64eqeq1d 2444 . . . . 5
76rexbidv 2719 . . . 4
85, 7imbi12d 312 . . 3
91, 8raleqbidv 2909 . 2
10 df-cmp 17443 . 2
119, 10elrab2 3087 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  wral 2698  wrex 2699   cin 3312  cpw 3792  cuni 4008  cfn 7102  ctop 16951  ccmp 17442 This theorem is referenced by:  cmpcov  17445  cncmp  17448  fincmp  17449  cmptop  17451  cmpsub  17456  tgcmp  17457  uncmp  17459  sscmp  17461  cmpfi  17464  bwth  17466  txcmp  17668  alexsubb  18070  alexsubALT  18075  onsucsuccmpi  26186  limsucncmpi  26188  comppfsc  26379  heibor  26522 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-in 3320  df-ss 3327  df-pw 3794  df-uni 4009  df-cmp 17443
 Copyright terms: Public domain W3C validator