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

Theorem iscmp 21391
 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 4303 . . 3 (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2 unieq 4594 . . . . . 6 (𝑥 = 𝐽 𝑥 = 𝐽)
3 iscmp.1 . . . . . 6 𝑋 = 𝐽
42, 3syl6eqr 2810 . . . . 5 (𝑥 = 𝐽 𝑥 = 𝑋)
54eqeq1d 2760 . . . 4 (𝑥 = 𝐽 → ( 𝑥 = 𝑦𝑋 = 𝑦))
64eqeq1d 2760 . . . . 5 (𝑥 = 𝐽 → ( 𝑥 = 𝑧𝑋 = 𝑧))
76rexbidv 3188 . . . 4 (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
85, 7imbi12d 333 . . 3 (𝑥 = 𝐽 → (( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
91, 8raleqbidv 3289 . 2 (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
10 df-cmp 21390 . 2 Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
119, 10elrab2 3505 1 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1630   ∈ wcel 2137  ∀wral 3048  ∃wrex 3049   ∩ cin 3712  𝒫 cpw 4300  ∪ cuni 4586  Fincfn 8119  Topctop 20898  Compccmp 21389 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-in 3720  df-ss 3727  df-pw 4302  df-uni 4587  df-cmp 21390 This theorem is referenced by:  cmpcov  21392  cncmp  21395  fincmp  21396  cmptop  21398  cmpsub  21403  tgcmp  21404  uncmp  21406  sscmp  21408  cmpfi  21411  comppfsc  21535  txcmp  21646  alexsubb  22049  alexsubALT  22054  cmpcref  30224  onsucsuccmpi  32746  limsucncmpi  32748  heibor  33931
 Copyright terms: Public domain W3C validator