Theorem cmptop 22003

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139   ∩ cin 3935  𝒫 cpw 4539  ∪ cuni 4838  Fincfn 8509  Topctop 21501  Compccmp 21994

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541  df-uni 4839  df-cmp 21995

This theorem is referenced by:  imacmp  22005  cmpcld  22010  fiuncmp  22012  cmpfii  22017  bwth  22018  locfincmp  22134  kgeni  22145  kgentopon  22146  kgencmp  22153  kgencmp2  22154  cmpkgen  22159  txcmplem1  22249  txcmp  22251  qtopcmp  22316  cmphaushmeo  22408  ptcmpfi  22421  fclscmpi  22637  alexsubALTlem1  22655  ptcmplem1  22660  ptcmpg  22665  evth  23563  evth2  23564  cmppcmp  31122  ordcmp  33795  poimirlem30  34937  heibor1lem  35102  cmpfiiin  39314  kelac1  39683  kelac2  39685  stoweidlem28  42333  stoweidlem50  42355  stoweidlem53  42358  stoweidlem57  42362  stoweidlem62  42367