Theorem cmptop 22454

Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)

Assertion

Ref	Expression
cmptop	⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)

Proof of Theorem cmptop

Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscmp 22447	. 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠)))
3	2	simplbi 497	1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   ∩ cin 3882  𝒫 cpw 4530  ∪ cuni 4836  Fincfn 8691  Topctop 21950  Compccmp 22445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532  df-uni 4837  df-cmp 22446

This theorem is referenced by:  imacmp  22456  cmpcld  22461  fiuncmp  22463  cmpfii  22468  bwth  22469  locfincmp  22585  kgeni  22596  kgentopon  22597  kgencmp  22604  kgencmp2  22605  cmpkgen  22610  txcmplem1  22700  txcmp  22702  qtopcmp  22767  cmphaushmeo  22859  ptcmpfi  22872  fclscmpi  23088  alexsubALTlem1  23106  ptcmplem1  23111  ptcmpg  23116  evth  24028  evth2  24029  cmppcmp  31710  ordcmp  34563  poimirlem30  35734  heibor1lem  35894  cmpfiiin  40435  kelac1  40804  kelac2  40806  stoweidlem28  43459  stoweidlem50  43481  stoweidlem53  43484  stoweidlem57  43488  stoweidlem62  43493