Theorem iscmp 23619

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 4574	. . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽)
2		unieq 4881	. . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽)
3		iscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
4	2, 3	eqtr4di 2815	. . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋)
5	4	eqeq1d 2764	. . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦))
6	4	eqeq1d 2764	. . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧))
7	6	rexbidv 3188	. . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
8	5, 7	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
9	1, 8	raleqbidv 3336	. 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
10		df-cmp 23618	. 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
11	9, 10	elrab2 3652	1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   ∩ cin 3901  𝒫 cpw 4560  ∪ cuni 4870  Fincfn 8956  Topctop 23124  Compccmp 23617

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-pw 4562  df-uni 4871  df-cmp 23618

This theorem is used by:  cmpcov  23620  cncmp  23623  fincmp  23624  cmptop  23626  cmpsub  23631  tgcmp  23632  uncmp  23634  sscmp  23636  cmpfi  23639  comppfsc  23764  txcmp  23875  alexsubb  24278  alexsubALT  24283  cmpcref  34368  onsucsuccmpi  37070  limsucncmpi  37072  pibp16  38175  heibor  38579