Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isref Unicode version

Theorem isref 26050
Description: The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 26039. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.)
Hypotheses
Ref Expression
isref.1  |-  X  = 
U. A
isref.2  |-  Y  = 
U. B
Assertion
Ref Expression
isref  |-  ( B  e.  C  ->  ( A Ref B  <->  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y
) ) )
Distinct variable groups:    x, y, A    x, B
Allowed substitution hints:    B( y)    C( x, y)    X( x, y)    Y( x, y)

Proof of Theorem isref
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 refrel 26049 . . . . 5  |-  Rel  Ref
21brrelexi 4858 . . . 4  |-  ( A Ref B  ->  A  e.  _V )
32adantl 453 . . 3  |-  ( ( B  e.  C  /\  A Ref B )  ->  A  e.  _V )
4 simpl 444 . . 3  |-  ( ( B  e.  C  /\  A Ref B )  ->  B  e.  C )
53, 4jca 519 . 2  |-  ( ( B  e.  C  /\  A Ref B )  -> 
( A  e.  _V  /\  B  e.  C ) )
6 simpr 448 . . . . . . 7  |-  ( ( B  e.  C  /\  X  =  Y )  ->  X  =  Y )
7 isref.1 . . . . . . 7  |-  X  = 
U. A
8 isref.2 . . . . . . 7  |-  Y  = 
U. B
96, 7, 83eqtr3g 2442 . . . . . 6  |-  ( ( B  e.  C  /\  X  =  Y )  ->  U. A  =  U. B )
10 uniexg 4646 . . . . . . 7  |-  ( B  e.  C  ->  U. B  e.  _V )
1110adantr 452 . . . . . 6  |-  ( ( B  e.  C  /\  X  =  Y )  ->  U. B  e.  _V )
129, 11eqeltrd 2461 . . . . 5  |-  ( ( B  e.  C  /\  X  =  Y )  ->  U. A  e.  _V )
13 uniexb 4692 . . . . 5  |-  ( A  e.  _V  <->  U. A  e. 
_V )
1412, 13sylibr 204 . . . 4  |-  ( ( B  e.  C  /\  X  =  Y )  ->  A  e.  _V )
1514adantrr 698 . . 3  |-  ( ( B  e.  C  /\  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y ) )  ->  A  e.  _V )
16 simpl 444 . . 3  |-  ( ( B  e.  C  /\  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y ) )  ->  B  e.  C
)
1715, 16jca 519 . 2  |-  ( ( B  e.  C  /\  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y ) )  ->  ( A  e. 
_V  /\  B  e.  C ) )
18 unieq 3966 . . . . . 6  |-  ( a  =  A  ->  U. a  =  U. A )
1918, 7syl6eqr 2437 . . . . 5  |-  ( a  =  A  ->  U. a  =  X )
2019eqeq1d 2395 . . . 4  |-  ( a  =  A  ->  ( U. a  =  U. b 
<->  X  =  U. b
) )
21 rexeq 2848 . . . . 5  |-  ( a  =  A  ->  ( E. y  e.  a  x  C_  y  <->  E. y  e.  A  x  C_  y
) )
2221ralbidv 2669 . . . 4  |-  ( a  =  A  ->  ( A. x  e.  b  E. y  e.  a  x  C_  y  <->  A. x  e.  b  E. y  e.  A  x  C_  y
) )
2320, 22anbi12d 692 . . 3  |-  ( a  =  A  ->  (
( U. a  = 
U. b  /\  A. x  e.  b  E. y  e.  a  x  C_  y )  <->  ( X  =  U. b  /\  A. x  e.  b  E. y  e.  A  x  C_  y ) ) )
24 unieq 3966 . . . . . 6  |-  ( b  =  B  ->  U. b  =  U. B )
2524, 8syl6eqr 2437 . . . . 5  |-  ( b  =  B  ->  U. b  =  Y )
2625eqeq2d 2398 . . . 4  |-  ( b  =  B  ->  ( X  =  U. b  <->  X  =  Y ) )
27 raleq 2847 . . . 4  |-  ( b  =  B  ->  ( A. x  e.  b  E. y  e.  A  x  C_  y  <->  A. x  e.  B  E. y  e.  A  x  C_  y
) )
2826, 27anbi12d 692 . . 3  |-  ( b  =  B  ->  (
( X  =  U. b  /\  A. x  e.  b  E. y  e.  A  x  C_  y
)  <->  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y
) ) )
29 df-ref 26035 . . 3  |-  Ref  =  { <. a ,  b
>.  |  ( U. a  =  U. b  /\  A. x  e.  b  E. y  e.  a  x  C_  y ) }
3023, 28, 29brabg 4415 . 2  |-  ( ( A  e.  _V  /\  B  e.  C )  ->  ( A Ref B  <->  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y ) ) )
315, 17, 30pm5.21nd 869 1  |-  ( B  e.  C  ->  ( A Ref B  <->  ( X  =  Y  /\  A. x  e.  B  E. y  e.  A  x  C_  y
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   E.wrex 2650   _Vcvv 2899    C_ wss 3263   U.cuni 3957   class class class wbr 4153   Refcref 26031
This theorem is referenced by:  refbas  26051  refssex  26052  ssref  26054  refref  26056  reftr  26060  fnessref  26064  refssfne  26065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-ref 26035
  Copyright terms: Public domain W3C validator