Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypothesis	iscmp.1	$$⊢X=\bigcup J$$
Assertion	iscmp	$$⊢J\in \mathrm{Comp}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	$$⊢X=\bigcup J$$
2		pweq	$$⊢x=J\to 𝒫x=𝒫J$$
3		unieq	$$⊢x=J\to \bigcup x=\bigcup J$$
4	3 1	eqtr4di	$$⊢x=J\to \bigcup x=X$$
5	4	eqeq1d	$$⊢x=J\to \left(\bigcup x=\bigcup y\leftrightarrow X=\bigcup y\right)$$
6	4	eqeq1d	$$⊢x=J\to \left(\bigcup x=\bigcup z\leftrightarrow X=\bigcup z\right)$$
7	6	rexbidv	$$⊢x=J\to \left(\exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\leftrightarrow \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)$$
8	5 7	imbi12d	$$⊢x=J\to \left(\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)\leftrightarrow \left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$
9	2 8	raleqbidv	$$⊢x=J\to \left(\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\bigcup x=\bigcup z\right)\leftrightarrow \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$
10		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\}$$
11	9 10	elrab2	$$⊢J\in \mathrm{Comp}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$