Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmsval Unicode version

Theorem cvmsval 24201
Description: Elementhood in the set  S of all even coverings of an open set in  J.  S is an even covering of  U if it is a nonempty collection of disjoint open sets in  C whose union is the preimage of  U, such that each set  u  e.  S is homeomorphic under  F to  U. (Contributed by Mario Carneiro, 13-Feb-2015.)
Hypothesis
Ref Expression
cvmcov.1  |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) ) ) } )
Assertion
Ref Expression
cvmsval  |-  ( C  e.  V  ->  ( T  e.  ( S `  U )  <->  ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
Distinct variable groups:    k, s, u, v, C    k, F, s, u, v    k, J, s, u, v    U, k, s, u, v    T, s, u, v    k, V, s, u, v
Allowed substitution hints:    S( v, u, k, s)    T( k)

Proof of Theorem cvmsval
StepHypRef Expression
1 cvmcov.1 . . 3  |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) ) ) } )
21cvmsi 24200 . 2  |-  ( T  e.  ( S `  U )  ->  ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) )
3 3anass 938 . . 3  |-  ( ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )  <->  ( U  e.  J  /\  (
( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
4 id 19 . . . . . . . 8  |-  ( U  e.  J  ->  U  e.  J )
5 pwexg 4275 . . . . . . . . 9  |-  ( C  e.  V  ->  ~P C  e.  _V )
6 difexg 4243 . . . . . . . . 9  |-  ( ~P C  e.  _V  ->  ( ~P C  \  { (/)
} )  e.  _V )
7 rabexg 4245 . . . . . . . . 9  |-  ( ( ~P C  \  { (/)
} )  e.  _V  ->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) }  e.  _V )
85, 6, 73syl 18 . . . . . . . 8  |-  ( C  e.  V  ->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) }  e.  _V )
9 imaeq2 5090 . . . . . . . . . . . 12  |-  ( k  =  U  ->  ( `' F " k )  =  ( `' F " U ) )
109eqeq2d 2369 . . . . . . . . . . 11  |-  ( k  =  U  ->  ( U. s  =  ( `' F " k )  <->  U. s  =  ( `' F " U ) ) )
11 oveq2 5953 . . . . . . . . . . . . . . 15  |-  ( k  =  U  ->  ( Jt  k )  =  ( Jt  U ) )
1211oveq2d 5961 . . . . . . . . . . . . . 14  |-  ( k  =  U  ->  (
( Ct  u )  Homeo  ( Jt  k ) )  =  ( ( Ct  u )  Homeo  ( Jt  U ) ) )
1312eleq2d 2425 . . . . . . . . . . . . 13  |-  ( k  =  U  ->  (
( F  |`  u
)  e.  ( ( Ct  u )  Homeo  ( Jt  k ) )  <->  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) )
1413anbi2d 684 . . . . . . . . . . . 12  |-  ( k  =  U  ->  (
( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) )  <->  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )
1514ralbidv 2639 . . . . . . . . . . 11  |-  ( k  =  U  ->  ( A. u  e.  s 
( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) )  <->  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )
1610, 15anbi12d 691 . . . . . . . . . 10  |-  ( k  =  U  ->  (
( U. s  =  ( `' F "
k )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) )  <-> 
( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) ) )
1716rabbidv 2856 . . . . . . . . 9  |-  ( k  =  U  ->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
k )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }  =  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) } )
1817, 1fvmptg 5683 . . . . . . . 8  |-  ( ( U  e.  J  /\  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) }  e.  _V )  ->  ( S `  U
)  =  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) } )
194, 8, 18syl2anr 464 . . . . . . 7  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( S `  U
)  =  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) } )
2019eleq2d 2425 . . . . . 6  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( T  e.  ( S `  U )  <-> 
T  e.  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) } ) )
21 unieq 3917 . . . . . . . . . 10  |-  ( s  =  T  ->  U. s  =  U. T )
2221eqeq1d 2366 . . . . . . . . 9  |-  ( s  =  T  ->  ( U. s  =  ( `' F " U )  <->  U. T  =  ( `' F " U ) ) )
23 difeq1 3363 . . . . . . . . . . . 12  |-  ( s  =  T  ->  (
s  \  { u } )  =  ( T  \  { u } ) )
2423raleqdv 2818 . . . . . . . . . . 11  |-  ( s  =  T  ->  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/) 
<-> 
A. v  e.  ( T  \  { u } ) ( u  i^i  v )  =  (/) ) )
2524anbi1d 685 . . . . . . . . . 10  |-  ( s  =  T  ->  (
( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) )  <-> 
( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )
2625raleqbi1dv 2820 . . . . . . . . 9  |-  ( s  =  T  ->  ( A. u  e.  s 
( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) )  <->  A. u  e.  T  ( A. v  e.  ( T  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) )
2722, 26anbi12d 691 . . . . . . . 8  |-  ( s  =  T  ->  (
( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) )  <-> 
( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  { u }
) ( u  i^i  v )  =  (/)  /\  ( F  |`  u
)  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) ) )
2827elrab 2999 . . . . . . 7  |-  ( T  e.  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  (
s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) }  <->  ( T  e.  ( ~P C  \  { (/) } )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) )
29 eldifsn 3825 . . . . . . . . 9  |-  ( T  e.  ( ~P C  \  { (/) } )  <->  ( T  e.  ~P C  /\  T  =/=  (/) ) )
30 elpw2g 4255 . . . . . . . . . . 11  |-  ( C  e.  V  ->  ( T  e.  ~P C  <->  T 
C_  C ) )
3130adantr 451 . . . . . . . . . 10  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( T  e.  ~P C 
<->  T  C_  C )
)
3231anbi1d 685 . . . . . . . . 9  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( ( T  e. 
~P C  /\  T  =/=  (/) )  <->  ( T  C_  C  /\  T  =/=  (/) ) ) )
3329, 32syl5bb 248 . . . . . . . 8  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( T  e.  ( ~P C  \  { (/)
} )  <->  ( T  C_  C  /\  T  =/=  (/) ) ) )
3433anbi1d 685 . . . . . . 7  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( ( T  e.  ( ~P C  \  { (/) } )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )  <->  ( ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
3528, 34syl5bb 248 . . . . . 6  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( T  e.  {
s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F " U )  /\  A. u  e.  s  ( A. v  e.  ( s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  U ) ) ) ) }  <->  ( ( T 
C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
3620, 35bitrd 244 . . . . 5  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( T  e.  ( S `  U )  <-> 
( ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
3736biimprd 214 . . . 4  |-  ( ( C  e.  V  /\  U  e.  J )  ->  ( ( ( T 
C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )  ->  T  e.  ( S `  U
) ) )
3837expimpd 586 . . 3  |-  ( C  e.  V  ->  (
( U  e.  J  /\  ( ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) )  ->  T  e.  ( S `  U ) ) )
393, 38syl5bi 208 . 2  |-  ( C  e.  V  ->  (
( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) )  ->  T  e.  ( S `  U
) ) )
402, 39impbid2 195 1  |-  ( C  e.  V  ->  ( T  e.  ( S `  U )  <->  ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U )  /\  A. u  e.  T  ( A. v  e.  ( T  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  U ) ) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710    =/= wne 2521   A.wral 2619   {crab 2623   _Vcvv 2864    \ cdif 3225    i^i cin 3227    C_ wss 3228   (/)c0 3531   ~Pcpw 3701   {csn 3716   U.cuni 3908    e. cmpt 4158   `'ccnv 4770    |` cres 4773   "cima 4774   ` cfv 5337  (class class class)co 5945   ↾t crest 13424    Homeo chmeo 17550
This theorem is referenced by:  cvmsss2  24209
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator