Metamath Proof Explorer

Theorem locfintop

Description: A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Assertion locfintop 
|- ( A e. ( LocFin ` J ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. A = U. A
3 1 2 islocfin 
 |-  ( A e. ( LocFin ` J ) <-> ( J e. Top /\ U. J = U. A /\ A. s e. U. J E. n e. J ( s e. n /\ { x e. A | ( x i^i n ) =/= (/) } e. Fin ) ) )
4 3 simp1bi 
 |-  ( A e. ( LocFin ` J ) -> J e. Top )