Theorem iscmp 23304

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 4563	. . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2		unieq 4869	. . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽)
3		iscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
4	2, 3	eqtr4di 2786	. . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋)
5	4	eqeq1d 2735	. . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦))
6	4	eqeq1d 2735	. . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧))
7	6	rexbidv 3157	. . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
8	5, 7	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
9	1, 8	raleqbidv 3313	. 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
10		df-cmp 23303	. 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
11	9, 10	elrab2 3646	1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057   ∩ cin 3897  𝒫 cpw 4549  ∪ cuni 4858  Fincfn 8875  Topctop 22809  Compccmp 23302

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-pw 4551  df-uni 4859  df-cmp 23303

This theorem is referenced by:  cmpcov  23305  cncmp  23308  fincmp  23309  cmptop  23311  cmpsub  23316  tgcmp  23317  uncmp  23319  sscmp  23321  cmpfi  23324  comppfsc  23448  txcmp  23559  alexsubb  23962  alexsubALT  23967  cmpcref  33884  onsucsuccmpi  36508  limsucncmpi  36510  pibp16  37478  heibor  37881