Theorem cmptop 23339

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060   ∩ cin 3900  𝒫 cpw 4554  ∪ cuni 4863  Fincfn 8883  Topctop 22837  Compccmp 23330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-ss 3918  df-pw 4556  df-uni 4864  df-cmp 23331

This theorem is referenced by:  imacmp  23341  cmpcld  23346  fiuncmp  23348  cmpfii  23353  bwth  23354  locfincmp  23470  kgeni  23481  kgentopon  23482  kgencmp  23489  kgencmp2  23490  cmpkgen  23495  txcmplem1  23585  txcmp  23587  qtopcmp  23652  cmphaushmeo  23744  ptcmpfi  23757  fclscmpi  23973  alexsubALTlem1  23991  ptcmplem1  23996  ptcmpg  24001  evth  24914  evth2  24915  cmppcmp  34015  ordcmp  36641  poimirlem30  37847  heibor1lem  38006  cmpfiiin  42935  kelac1  43301  kelac2  43303  stoweidlem28  46268  stoweidlem50  46290  stoweidlem53  46293  stoweidlem57  46297  stoweidlem62  46302