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 = U. J
Assertion	iscmp	|- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	|- X = U. J
2		pweq	|- ( x = J -> ~P x = ~P J )
3		unieq	|- ( x = J -> U. x = U. J )
4	3 1	eqtr4di	|- ( x = J -> U. x = X )
5	4	eqeq1d	|- ( x = J -> ( U. x = U. y <-> X = U. y ) )
6	4	eqeq1d	|- ( x = J -> ( U. x = U. z <-> X = U. z ) )
7	6	rexbidv	|- ( x = J -> ( E. z e. ( ~P y i^i Fin ) U. x = U. z <-> E. z e. ( ~P y i^i Fin ) X = U. z ) )
8	5 7	imbi12d	|- ( x = J -> ( ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
9	2 8	raleqbidv	|- ( x = J -> ( A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
10		df-cmp	|- Comp = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
11	9 10	elrab2	|- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )