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

Theorem iscmp 22776
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 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Distinct variable group:   𝑦,𝑧,𝐽
Allowed substitution hints:   𝑋(𝑦,𝑧)

Proof of Theorem iscmp
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pweq 4579 . . 3 (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2 unieq 4881 . . . . . 6 (𝑥 = 𝐽 𝑥 = 𝐽)
3 iscmp.1 . . . . . 6 𝑋 = 𝐽
42, 3eqtr4di 2789 . . . . 5 (𝑥 = 𝐽 𝑥 = 𝑋)
54eqeq1d 2733 . . . 4 (𝑥 = 𝐽 → ( 𝑥 = 𝑦𝑋 = 𝑦))
64eqeq1d 2733 . . . . 5 (𝑥 = 𝐽 → ( 𝑥 = 𝑧𝑋 = 𝑧))
76rexbidv 3171 . . . 4 (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
85, 7imbi12d 344 . . 3 (𝑥 = 𝐽 → (( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
91, 8raleqbidv 3317 . 2 (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
10 df-cmp 22775 . 2 Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
119, 10elrab2 3651 1 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3060  wrex 3069  cin 3912  𝒫 cpw 4565   cuni 4870  Fincfn 8890  Topctop 22279  Compccmp 22774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567  df-uni 4871  df-cmp 22775
This theorem is referenced by:  cmpcov  22777  cncmp  22780  fincmp  22781  cmptop  22783  cmpsub  22788  tgcmp  22789  uncmp  22791  sscmp  22793  cmpfi  22796  comppfsc  22920  txcmp  23031  alexsubb  23434  alexsubALT  23439  cmpcref  32520  onsucsuccmpi  34991  limsucncmpi  34993  pibp16  35957  heibor  36353
  Copyright terms: Public domain W3C validator