MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islocfin Structured version   Visualization version   Unicode version
Theorem islocfin 21320
Description: The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.)
Hypotheses
Ref Expression
islocfin.1 |- X = U. J
islocfin.2 |- Y = U. A
Assertion
Ref Expression
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 ) ) )
Distinct variable groups:   n, s, x, A   n, J, x   x, X
Allowed substitution hints:   J( s)   X( n, s)   Y( x, n, s)
Proof of Theorem islocfin
Dummy variables j y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-locfin 21310 . . . . 5 |- 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 ) ) } )
21dmmptss 5631 . . . 4 |- dom LocFin C_ Top
3 elfvdm 6220 . . . 4 |- ( A e. ( LocFin ` J ) -> J e. dom LocFin )
42, 3sseldi 3601 . . 3 |- ( A e. ( LocFin ` J ) -> J e. Top )
5 eqimss2 3658 . . . . . . . . . . 11 |- ( X = U. y -> U. y C_ X )
6 sspwuni 4611 . . . . . . . . . . 11 |- ( y C_ ~P X <-> U. y C_ X )
75, 6sylibr 224 . . . . . . . . . 10 |- ( X = U. y -> y C_ ~P X )
8 selpw 4165 . . . . . . . . . 10 |- ( y e. ~P ~P X <-> y C_ ~P X )
97, 8sylibr 224 . . . . . . . . 9 |- ( X = U. y -> y e. ~P ~P X )
109adantr 481 . . . . . . . 8 |- ( ( 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 )
1110abssi 3677 . . . . . . 7 |- { 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 islocfin.1 . . . . . . . . 9 |- X = U. J
1312topopn 20711 . . . . . . . 8 |- ( J e. Top -> X e. J )
14 pwexg 4850 . . . . . . . 8 |- ( X e. J -> ~P X e. _V )
15 pwexg 4850 . . . . . . . 8 |- ( ~P X e. _V -> ~P ~P X e. _V )
1613, 14, 153syl 18 . . . . . . 7 |- ( J e. Top -> ~P ~P X e. _V )
17 ssexg 4804 . . . . . . 7 |- ( ( { 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 )
1811, 16, 17sylancr 695 . . . . . 6 |- ( 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 )
19 unieq 4444 . . . . . . . . . . 11 |- ( j = J -> U. j = U. J )
2019, 12syl6eqr 2674 . . . . . . . . . 10 |- ( j = J -> U. j = X )
2120eqeq1d 2624 . . . . . . . . 9 |- ( j = J -> ( U. j = U. y <-> X = U. y ) )
22 rexeq 3139 . . . . . . . . . 10 |- ( 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 ) ) )
2320, 22raleqbidv 3152 . . . . . . . . 9 |- ( 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 ) ) )
2421, 23anbi12d 747 . . . . . . . 8 |- ( 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 ) ) ) )
2524abbidv 2741 . . . . . . 7 |- ( 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 ) ) } )
2625, 1fvmptg 6280 . . . . . 6 |- ( ( 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 ) ) } )
2718, 26mpdan 702 . . . . 5 |- ( 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 ) ) } )
2827eleq2d 2687 . . . 4 |- ( 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 ) ) } ) )
29 elex 3212 . . . . . 6 |- ( 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 )
3029adantl 482 . . . . 5 |- ( ( 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 )
31 simpr 477 . . . . . . . . . 10 |- ( ( J e. Top /\ X = Y ) -> X = Y )
32 islocfin.2 . . . . . . . . . 10 |- Y = U. A
3331, 32syl6eq 2672 . . . . . . . . 9 |- ( ( J e. Top /\ X = Y ) -> X = U. A )
3413adantr 481 . . . . . . . . 9 |- ( ( J e. Top /\ X = Y ) -> X e. J )
3533, 34eqeltrrd 2702 . . . . . . . 8 |- ( ( J e. Top /\ X = Y ) -> U. A e. J )
36 elex 3212 . . . . . . . 8 |- ( U. A e. J -> U. A e. _V )
3735, 36syl 17 . . . . . . 7 |- ( ( J e. Top /\ X = Y ) -> U. A e. _V )
38 uniexb 6973 . . . . . . 7 |- ( A e. _V <-> U. A e. _V )
3937, 38sylibr 224 . . . . . 6 |- ( ( J e. Top /\ X = Y ) -> A e. _V )
4039adantrr 753 . . . . 5 |- ( ( 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 )
41 unieq 4444 . . . . . . . . 9 |- ( y = A -> U. y = U. A )
4241, 32syl6eqr 2674 . . . . . . . 8 |- ( y = A -> U. y = Y )
4342eqeq2d 2632 . . . . . . 7 |- ( y = A -> ( X = U. y <-> X = Y ) )
44 rabeq 3192 . . . . . . . . . . 11 |- ( y = A -> { s e. y | ( s i^i n ) =/= (/) } = { s e. A | ( s i^i n ) =/= (/) } )
4544eleq1d 2686 . . . . . . . . . 10 |- ( y = A -> ( { s e. y | ( s i^i n ) =/= (/) } e. Fin <-> { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
4645anbi2d 740 . . . . . . . . 9 |- ( 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 ) ) )
4746rexbidv 3052 . . . . . . . 8 |- ( 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 ) ) )
4847ralbidv 2986 . . . . . . 7 |- ( 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 ) ) )
4943, 48anbi12d 747 . . . . . 6 |- ( 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 ) ) ) )
5049elabg 3351 . . . . 5 |- ( 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 ) ) ) )
5130, 40, 50pm5.21nd 941 . . . 4 |- ( 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 ) ) ) )
5228, 51bitrd 268 . . 3 |- ( 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 ) ) ) )
534, 52biadan2 674 . 2 |- ( 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 ) ) ) )
54 3anass 1042 . 2 |- ( ( 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 ) ) ) )
5553, 54bitr4i 267 1 |- ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   dom cdm 5114   ` cfv 5888   Fincfn 7955   Topctop 20698   LocFinclocfin 21307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896  df-top 20699  df-locfin 21310
This theorem is referenced by:  finlocfin  21323  locfintop  21324  locfinbas  21325  locfinnei  21326  lfinun  21328  dissnlocfin  21332  locfindis  21333  locfincf  21334  locfinreflem  29907  locfinref  29908
  Copyright terms: Public domain W3C validator