Metamath Proof Explorer

Theorem islocfin

Description: The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypotheses islocfin.1 
|- X = U. J
islocfin.2 
|- Y = U. A
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 islocfin.1 
 |-  X = U. J
2 islocfin.2 
 |-  Y = U. A
3 df-locfin 
 |-  LocFin = ( j e. Top |-> { y | ( U. j = U. y /\ A. x e. U. j E. n e. j ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } )
4 3 mptrcl 
 |-  ( A e. ( LocFin ` J ) -> J e. Top )
5 eqimss2 
 |-  ( X = U. y -> U. y C_ X )
6 sspwuni 
 |-  ( y C_ ~P X <-> U. y C_ X )
7 5 6 sylibr 
 |-  ( X = U. y -> y C_ ~P X )
8 velpw 
 |-  ( y e. ~P ~P X <-> y C_ ~P X )
9 7 8 sylibr 
 |-  ( X = U. y -> y e. ~P ~P X )
10 9 adantr 
 |-  ( ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) -> y e. ~P ~P X )
11 10 abssi 
 |-  { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } C_ ~P ~P X
12 1 topopn 
 |-  ( J e. Top -> X e. J )
13 pwexg 
 |-  ( X e. J -> ~P X e. _V )
14 pwexg 
 |-  ( ~P X e. _V -> ~P ~P X e. _V )
15 12 13 14 3syl 
 |-  ( J e. Top -> ~P ~P X e. _V )
16 ssexg 
 |-  ( ( { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } C_ ~P ~P X /\ ~P ~P X e. _V ) -> { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } e. _V )
17 11 15 16 sylancr 
 |-  ( J e. Top -> { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } e. _V )
18 unieq 
 |-  ( j = J -> U. j = U. J )
19 18 1 eqtr4di 
 |-  ( j = J -> U. j = X )
20 19 eqeq1d 
 |-  ( j = J -> ( U. j = U. y <-> X = U. y ) )
21 rexeq 
 |-  ( j = J -> ( E. n e. j ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) <-> E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) )
22 19 21 raleqbidv 
 |-  ( j = J -> ( A. x e. U. j E. n e. j ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) <-> A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) )
23 20 22 anbi12d 
 |-  ( j = J -> ( ( U. j = U. y /\ A. x e. U. j E. n e. j ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) <-> ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) ) )
24 23 abbidv 
 |-  ( j = J -> { y | ( U. j = U. y /\ A. x e. U. j E. n e. j ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } = { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } )
25 24 3 fvmptg 
 |-  ( ( J e. Top /\ { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } e. _V ) -> ( LocFin ` J ) = { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } )
26 17 25 mpdan 
 |-  ( J e. Top -> ( LocFin ` J ) = { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } )
27 26 eleq2d 
 |-  ( J e. Top -> ( A e. ( LocFin ` J ) <-> A e. { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } ) )
28 elex 
 |-  ( A e. { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } -> A e. _V )
29 28 adantl 
 |-  ( ( J e. Top /\ A e. { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } ) -> A e. _V )
30 simpr 
 |-  ( ( J e. Top /\ X = Y ) -> X = Y )
31 30 2 eqtrdi 
 |-  ( ( J e. Top /\ X = Y ) -> X = U. A )
32 12 adantr 
 |-  ( ( J e. Top /\ X = Y ) -> X e. J )
33 31 32 eqeltrrd 
 |-  ( ( J e. Top /\ X = Y ) -> U. A e. J )
34 33 elexd 
 |-  ( ( J e. Top /\ X = Y ) -> U. A e. _V )
35 uniexb 
 |-  ( A e. _V <-> U. A e. _V )
36 34 35 sylibr 
 |-  ( ( J e. Top /\ X = Y ) -> A e. _V )
37 36 adantrr 
 |-  ( ( 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 ) ) ) -> A e. _V )
38 unieq 
 |-  ( y = A -> U. y = U. A )
39 38 2 eqtr4di 
 |-  ( y = A -> U. y = Y )
40 39 eqeq2d 
 |-  ( y = A -> ( X = U. y <-> X = Y ) )
41 rabeq 
 |-  ( y = A -> { s e. y | ( s i^i n ) =/= (/) } = { s e. A | ( s i^i n ) =/= (/) } )
42 41 eleq1d 
 |-  ( y = A -> ( { s e. y | ( s i^i n ) =/= (/) } e. Fin <-> { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
43 42 anbi2d 
 |-  ( y = A -> ( ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) <-> ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
44 43 rexbidv 
 |-  ( y = A -> ( E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) <-> E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
45 44 ralbidv 
 |-  ( y = A -> ( A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) <-> A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
46 40 45 anbi12d 
 |-  ( y = A -> ( ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) <-> ( X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) ) )
47 46 elabg 
 |-  ( A e. _V -> ( A e. { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } <-> ( X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) ) )
48 29 37 47 pm5.21nd 
 |-  ( J e. Top -> ( A e. { y | ( X = U. y /\ A. x e. X E. n e. J ( x e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin ) ) } <-> ( X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) ) )
49 27 48 bitrd 
 |-  ( J e. Top -> ( A e. ( LocFin ` J ) <-> ( X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) ) )
50 4 49 biadanii 
 |-  ( 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 ) ) ) )
51 3anass 
 |-  ( ( 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 ) ) <-> ( 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 ) ) ) )
52 50 51 bitr4i 
 |-  ( 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 ) ) )