Definition df-cmp

Description: Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite subcovering (Heine-Borel property). Definition C''' of BourbakiTop1 p. I.59. Note: Bourbaki uses the term "quasi-compact" (saving "compact" for "compact Hausdorff"), but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008)

	Ref	Expression
Assertion	df-cmp	$$⊢\mathrm{Comp}=\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmp	$$class\mathrm{Comp}$$
1		vx	$$setvarx$$
2		ctop	$$class\mathrm{Top}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5	4	cpw	$$class𝒫x$$
6	4	cuni	$$class\bigcup x$$
7	3	cv	$$setvary$$
8	7	cuni	$$class\bigcup y$$
9	6 8	wceq	$$wff\bigcup x=\bigcup y$$
10		vz	$$setvarz$$
11	7	cpw	$$class𝒫y$$
12		cfn	$$class\mathrm{Fin}$$
13	11 12	cin	$$class\left(𝒫y\cap \mathrm{Fin}\right)$$
14	10	cv	$$setvarz$$
15	14	cuni	$$class\bigcup z$$
16	6 15	wceq	$$wff\bigcup x=\bigcup z$$
17	16 10 13	wrex	$$wff\exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z$$
18	9 17	wi	$$wff\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)$$
19	18 3 5	wral	$$wff\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)$$
20	19 1 2	crab	$$class\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)\right\}$$
21	0 20	wceq	$$wff\mathrm{Comp}=\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)\right\}$$