Theorem iscmp 23380

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 4611	. . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2		unieq 4916	. . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽)
3		iscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
4	2, 3	eqtr4di 2784	. . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋)
5	4	eqeq1d 2728	. . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦))
6	4	eqeq1d 2728	. . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧))
7	6	rexbidv 3169	. . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
8	5, 7	imbi12d 343	. . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
9	1, 8	raleqbidv 3330	. 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
10		df-cmp 23379	. 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
11	9, 10	elrab2 3683	1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ∀wral 3051  ∃wrex 3060   ∩ cin 3945  𝒫 cpw 4597  ∪ cuni 4905  Fincfn 8966  Topctop 22883  Compccmp 23378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-ss 3963  df-pw 4599  df-uni 4906  df-cmp 23379

This theorem is referenced by:  cmpcov  23381  cncmp  23384  fincmp  23385  cmptop  23387  cmpsub  23392  tgcmp  23393  uncmp  23395  sscmp  23397  cmpfi  23400  comppfsc  23524  txcmp  23635  alexsubb  24038  alexsubALT  24043  cmpcref  33678  onsucsuccmpi  36168  limsucncmpi  36170  pibp16  37133  heibor  37535