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

Theorem iscmp 22892
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 4617 . . 3 (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2 unieq 4920 . . . . . 6 (𝑥 = 𝐽 𝑥 = 𝐽)
3 iscmp.1 . . . . . 6 𝑋 = 𝐽
42, 3eqtr4di 2791 . . . . 5 (𝑥 = 𝐽 𝑥 = 𝑋)
54eqeq1d 2735 . . . 4 (𝑥 = 𝐽 → ( 𝑥 = 𝑦𝑋 = 𝑦))
64eqeq1d 2735 . . . . 5 (𝑥 = 𝐽 → ( 𝑥 = 𝑧𝑋 = 𝑧))
76rexbidv 3179 . . . 4 (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
85, 7imbi12d 345 . . 3 (𝑥 = 𝐽 → (( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
91, 8raleqbidv 3343 . 2 (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
10 df-cmp 22891 . 2 Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
119, 10elrab2 3687 1 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  cin 3948  𝒫 cpw 4603   cuni 4909  Fincfn 8939  Topctop 22395  Compccmp 22890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605  df-uni 4910  df-cmp 22891
This theorem is referenced by:  cmpcov  22893  cncmp  22896  fincmp  22897  cmptop  22899  cmpsub  22904  tgcmp  22905  uncmp  22907  sscmp  22909  cmpfi  22912  comppfsc  23036  txcmp  23147  alexsubb  23550  alexsubALT  23555  cmpcref  32830  onsucsuccmpi  35328  limsucncmpi  35330  pibp16  36294  heibor  36689
  Copyright terms: Public domain W3C validator