Metamath Proof Explorer

Theorem finlocfin

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

Ref Expression
Hypotheses finlocfin.1 
|- X = U. J
finlocfin.2 
|- Y = U. A
Assertion finlocfin 
|- ( ( J e. Top /\ A e. Fin /\ X = Y ) -> A e. ( LocFin ` J ) )

Proof

Step Hyp Ref Expression
1 finlocfin.1 
 |-  X = U. J
2 finlocfin.2 
 |-  Y = U. A
3 simp1 
 |-  ( ( J e. Top /\ A e. Fin /\ X = Y ) -> J e. Top )
4 simp3 
 |-  ( ( J e. Top /\ A e. Fin /\ X = Y ) -> X = Y )
5 simpl1 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> J e. Top )
6 1 topopn 
 |-  ( J e. Top -> X e. J )
7 5 6 syl 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> X e. J )
8 simpr 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> x e. X )
9 simpl2 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> A e. Fin )
10 ssrab2 
 |-  { s e. A | ( s i^i X ) =/= (/) } C_ A
11 ssfi 
 |-  ( ( A e. Fin /\ { s e. A | ( s i^i X ) =/= (/) } C_ A ) -> { s e. A | ( s i^i X ) =/= (/) } e. Fin )
12 9 10 11 sylancl 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> { s e. A | ( s i^i X ) =/= (/) } e. Fin )
13 eleq2 
 |-  ( n = X -> ( x e. n <-> x e. X ) )
14 ineq2 
 |-  ( n = X -> ( s i^i n ) = ( s i^i X ) )
15 14 neeq1d 
 |-  ( n = X -> ( ( s i^i n ) =/= (/) <-> ( s i^i X ) =/= (/) ) )
16 15 rabbidv 
 |-  ( n = X -> { s e. A | ( s i^i n ) =/= (/) } = { s e. A | ( s i^i X ) =/= (/) } )
17 16 eleq1d 
 |-  ( n = X -> ( { s e. A | ( s i^i n ) =/= (/) } e. Fin <-> { s e. A | ( s i^i X ) =/= (/) } e. Fin ) )
18 13 17 anbi12d 
 |-  ( n = X -> ( ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) <-> ( x e. X /\ { s e. A | ( s i^i X ) =/= (/) } e. Fin ) ) )
19 18 rspcev 
 |-  ( ( X e. J /\ ( x e. X /\ { s e. A | ( s i^i X ) =/= (/) } e. Fin ) ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
20 7 8 12 19 syl12anc 
 |-  ( ( ( J e. Top /\ A e. Fin /\ X = Y ) /\ x e. X ) -> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
21 20 ralrimiva 
 |-  ( ( J e. Top /\ A e. Fin /\ X = Y ) -> A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
22 1 2 islocfin 
 |-  ( A e. ( LocFin ` J ) <-> ( J e. Top /\ X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
23 3 4 21 22 syl3anbrc 
 |-  ( ( J e. Top /\ A e. Fin /\ X = Y ) -> A e. ( LocFin ` J ) )