Theorem pibt1

Description: Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 and pibp19 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020)

	Ref	Expression
Hypothesis	pibt1.19	|- C = { x e. Top | A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
Assertion	pibt1	|- ( J e. Comp -> J e. C )

Proof

Step	Hyp	Ref	Expression
1		pibt1.19	|- C = { x e. Top | A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
2		pm3.41	|- ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) -> ( ( U. J = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) )
3	2	ralimi	|- ( A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) -> A. y e. ~P J ( ( U. J = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) )
4	3	anim2i	|- ( ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) -> ( J e. Top /\ A. y e. ~P J ( ( U. J = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
5		eqid	|- U. J = U. J
6	5	pibp16	|- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
7	5 1	pibp19	|- ( J e. C <-> ( J e. Top /\ A. y e. ~P J ( ( U. J = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
8	4 6 7	3imtr4i	|- ( J e. Comp -> J e. C )