Theorem iscmp 23301

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.

Step	Hyp	Ref	Expression
1		pweq 4564	. . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2		unieq 4870	. . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽)
3		iscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
4	2, 3	eqtr4di 2784	. . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋)
5	4	eqeq1d 2733	. . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦))
6	4	eqeq1d 2733	. . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧))
7	6	rexbidv 3156	. . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
8	5, 7	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
9	1, 8	raleqbidv 3312	. 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
10		df-cmp 23300	. 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
11	9, 10	elrab2 3650	1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   ∩ cin 3901  𝒫 cpw 4550  ∪ cuni 4859  Fincfn 8869  Topctop 22806  Compccmp 23299

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-pw 4552  df-uni 4860  df-cmp 23300

This theorem is referenced by:  cmpcov  23302  cncmp  23305  fincmp  23306  cmptop  23308  cmpsub  23313  tgcmp  23314  uncmp  23316  sscmp  23318  cmpfi  23321  comppfsc  23445  txcmp  23556  alexsubb  23959  alexsubALT  23964  cmpcref  33858  onsucsuccmpi  36476  limsucncmpi  36478  pibp16  37446  heibor  37860