Theorem iscomp 11114

Description: The predicate "is a compact topology".

Assertion

Ref	Expression
iscomp	⊢ (J ∈ Comp ↔ (J ∈ Top ⋀ ∀y ∈ ℘ J(∪J = ∪y → ∃z ∈ (℘y ∩ Fin)∪J = ∪z)))

Distinct variable group:   y,J,z

Proof of Theorem iscomp

Step	Hyp	Ref	Expression
1		pweq 2460	. . 3 ⊢ (x = J → ℘x = ℘J)
2		unieq 2576	. . . . 5 ⊢ (x = J → ∪x = ∪J)
3	2	eqeq1d 1526	. . . 4 ⊢ (x = J → (∪x = ∪y ↔ ∪J = ∪y))
4	2	eqeq1d 1526	. . . . 5 ⊢ (x = J → (∪x = ∪z ↔ ∪J = ∪z))
5	4	rexbidv 1710	. . . 4 ⊢ (x = J → (∃z ∈ (℘y ∩ Fin)∪x = ∪z ↔ ∃z ∈ (℘y ∩ Fin)∪J = ∪z))
6	3, 5	imbi12d 629	. . 3 ⊢ (x = J → ((∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z) ↔ (∪J = ∪y → ∃z ∈ (℘y ∩ Fin)∪J = ∪z)))
7	1, 6	raleq12d 1840	. 2 ⊢ (x = J → (∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z) ↔ ∀y ∈ ℘ J(∪J = ∪y → ∃z ∈ (℘y ∩ Fin)∪J = ∪z)))
8		df-comp 11113	. 2 ⊢ Comp = {x ∈ Top∣∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)}
9	7, 8	elrab2 1953	1 ⊢ (J ∈ Comp ↔ (J ∈ Top ⋀ ∀y ∈ ℘ J(∪J = ∪y → ∃z ∈ (℘y ∩ Fin)∪J = ∪z)))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   = wceq 992   ∈ wcel 994  ∀wral 1691  ∃wrex 1692   ∩ cin 2098  ℘cpw 2458  ∪cuni 2569  Fincfn 4508  Topctop 7800  Compccomp 11112

This theorem is referenced by:  fintopcomp 11115  cmptop 11121  bwt2 11123  comptop 11485  compcov 11486  compsub 11488  uncomp 11490  compfipin0 11493  cncomp 11494  alexsub 11500  comppfsc 11578  heiborlem1 12011  heiborlem9 12019  heiborlem42 12052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-in 2103  df-ss 2105  df-pw 2459  df-uni 2570  df-comp 11113

Copyright terms: Public domain