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

Theorem iscmp 23396
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 4614 . . 3 (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2 unieq 4918 . . . . . 6 (𝑥 = 𝐽 𝑥 = 𝐽)
3 iscmp.1 . . . . . 6 𝑋 = 𝐽
42, 3eqtr4di 2795 . . . . 5 (𝑥 = 𝐽 𝑥 = 𝑋)
54eqeq1d 2739 . . . 4 (𝑥 = 𝐽 → ( 𝑥 = 𝑦𝑋 = 𝑦))
64eqeq1d 2739 . . . . 5 (𝑥 = 𝐽 → ( 𝑥 = 𝑧𝑋 = 𝑧))
76rexbidv 3179 . . . 4 (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
85, 7imbi12d 344 . . 3 (𝑥 = 𝐽 → (( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
91, 8raleqbidv 3346 . 2 (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
10 df-cmp 23395 . 2 Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
119, 10elrab2 3695 1 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  wrex 3070  cin 3950  𝒫 cpw 4600   cuni 4907  Fincfn 8985  Topctop 22899  Compccmp 23394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908  df-cmp 23395
This theorem is referenced by:  cmpcov  23397  cncmp  23400  fincmp  23401  cmptop  23403  cmpsub  23408  tgcmp  23409  uncmp  23411  sscmp  23413  cmpfi  23416  comppfsc  23540  txcmp  23651  alexsubb  24054  alexsubALT  24059  cmpcref  33849  onsucsuccmpi  36444  limsucncmpi  36446  pibp16  37414  heibor  37828
  Copyright terms: Public domain W3C validator