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

Theorem iscmp 23412
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 4619 . . 3 (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2 unieq 4923 . . . . . 6 (𝑥 = 𝐽 𝑥 = 𝐽)
3 iscmp.1 . . . . . 6 𝑋 = 𝐽
42, 3eqtr4di 2793 . . . . 5 (𝑥 = 𝐽 𝑥 = 𝑋)
54eqeq1d 2737 . . . 4 (𝑥 = 𝐽 → ( 𝑥 = 𝑦𝑋 = 𝑦))
64eqeq1d 2737 . . . . 5 (𝑥 = 𝐽 → ( 𝑥 = 𝑧𝑋 = 𝑧))
76rexbidv 3177 . . . 4 (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
85, 7imbi12d 344 . . 3 (𝑥 = 𝐽 → (( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
91, 8raleqbidv 3344 . 2 (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
10 df-cmp 23411 . 2 Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
119, 10elrab2 3698 1 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  wrex 3068  cin 3962  𝒫 cpw 4605   cuni 4912  Fincfn 8984  Topctop 22915  Compccmp 23410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-ss 3980  df-pw 4607  df-uni 4913  df-cmp 23411
This theorem is referenced by:  cmpcov  23413  cncmp  23416  fincmp  23417  cmptop  23419  cmpsub  23424  tgcmp  23425  uncmp  23427  sscmp  23429  cmpfi  23432  comppfsc  23556  txcmp  23667  alexsubb  24070  alexsubALT  24075  cmpcref  33811  onsucsuccmpi  36426  limsucncmpi  36428  pibp16  37396  heibor  37808
  Copyright terms: Public domain W3C validator