Theorem cmptop 23424

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 2740	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscmp 23417	. 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠)))
3	2	simplbi 497	1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076   ∩ cin 3975  𝒫 cpw 4622  ∪ cuni 4931  Fincfn 9003  Topctop 22920  Compccmp 23415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-ss 3993  df-pw 4624  df-uni 4932  df-cmp 23416

This theorem is referenced by:  imacmp  23426  cmpcld  23431  fiuncmp  23433  cmpfii  23438  bwth  23439  locfincmp  23555  kgeni  23566  kgentopon  23567  kgencmp  23574  kgencmp2  23575  cmpkgen  23580  txcmplem1  23670  txcmp  23672  qtopcmp  23737  cmphaushmeo  23829  ptcmpfi  23842  fclscmpi  24058  alexsubALTlem1  24076  ptcmplem1  24081  ptcmpg  24086  evth  25010  evth2  25011  cmppcmp  33804  ordcmp  36413  poimirlem30  37610  heibor1lem  37769  cmpfiiin  42653  kelac1  43020  kelac2  43022  stoweidlem28  45949  stoweidlem50  45971  stoweidlem53  45974  stoweidlem57  45978  stoweidlem62  45983