MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isref Structured version   Unicode version

Theorem isref 20136
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 30341. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
Hypotheses
Ref Expression
isref.1  |-  X  = 
U. A
isref.2  |-  Y  = 
U. B
Assertion
Ref Expression
isref  |-  ( A  e.  C  ->  ( A Ref B  <->  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y
) ) )
Distinct variable groups:    x, A    x, y, B
Allowed substitution hints:    A( 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 20135 . . . 4  |-  Rel  Ref
21brrelex2i 5050 . . 3  |-  ( A Ref B  ->  B  e.  _V )
32anim2i 569 . 2  |-  ( ( A  e.  C  /\  A Ref B )  -> 
( A  e.  C  /\  B  e.  _V ) )
4 simpl 457 . . 3  |-  ( ( A  e.  C  /\  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y ) )  ->  A  e.  C
)
5 simpr 461 . . . . . . 7  |-  ( ( A  e.  C  /\  Y  =  X )  ->  Y  =  X )
6 isref.2 . . . . . . 7  |-  Y  = 
U. B
7 isref.1 . . . . . . 7  |-  X  = 
U. A
85, 6, 73eqtr3g 2521 . . . . . 6  |-  ( ( A  e.  C  /\  Y  =  X )  ->  U. B  =  U. A )
9 uniexg 6596 . . . . . . 7  |-  ( A  e.  C  ->  U. A  e.  _V )
109adantr 465 . . . . . 6  |-  ( ( A  e.  C  /\  Y  =  X )  ->  U. A  e.  _V )
118, 10eqeltrd 2545 . . . . 5  |-  ( ( A  e.  C  /\  Y  =  X )  ->  U. B  e.  _V )
12 uniexb 6609 . . . . 5  |-  ( B  e.  _V  <->  U. B  e. 
_V )
1311, 12sylibr 212 . . . 4  |-  ( ( A  e.  C  /\  Y  =  X )  ->  B  e.  _V )
1413adantrr 716 . . 3  |-  ( ( A  e.  C  /\  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y ) )  ->  B  e.  _V )
154, 14jca 532 . 2  |-  ( ( A  e.  C  /\  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y ) )  ->  ( A  e.  C  /\  B  e. 
_V ) )
16 unieq 4259 . . . . . 6  |-  ( a  =  A  ->  U. a  =  U. A )
1716, 7syl6eqr 2516 . . . . 5  |-  ( a  =  A  ->  U. a  =  X )
1817eqeq2d 2471 . . . 4  |-  ( a  =  A  ->  ( U. b  =  U. a 
<-> 
U. b  =  X ) )
19 raleq 3054 . . . 4  |-  ( a  =  A  ->  ( A. x  e.  a  E. y  e.  b  x  C_  y  <->  A. x  e.  A  E. y  e.  b  x  C_  y
) )
2018, 19anbi12d 710 . . 3  |-  ( a  =  A  ->  (
( U. b  = 
U. a  /\  A. x  e.  a  E. y  e.  b  x  C_  y )  <->  ( U. b  =  X  /\  A. x  e.  A  E. y  e.  b  x  C_  y ) ) )
21 unieq 4259 . . . . . 6  |-  ( b  =  B  ->  U. b  =  U. B )
2221, 6syl6eqr 2516 . . . . 5  |-  ( b  =  B  ->  U. b  =  Y )
2322eqeq1d 2459 . . . 4  |-  ( b  =  B  ->  ( U. b  =  X  <->  Y  =  X ) )
24 rexeq 3055 . . . . 5  |-  ( b  =  B  ->  ( E. y  e.  b  x  C_  y  <->  E. y  e.  B  x  C_  y
) )
2524ralbidv 2896 . . . 4  |-  ( b  =  B  ->  ( A. x  e.  A  E. y  e.  b  x  C_  y  <->  A. x  e.  A  E. y  e.  B  x  C_  y
) )
2623, 25anbi12d 710 . . 3  |-  ( b  =  B  ->  (
( U. b  =  X  /\  A. x  e.  A  E. y  e.  b  x  C_  y
)  <->  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y
) ) )
27 df-ref 20132 . . 3  |-  Ref  =  { <. a ,  b
>.  |  ( U. b  =  U. a  /\  A. x  e.  a  E. y  e.  b  x  C_  y ) }
2820, 26, 27brabg 4775 . 2  |-  ( ( A  e.  C  /\  B  e.  _V )  ->  ( A Ref B  <->  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y ) ) )
293, 15, 28pm5.21nd 900 1  |-  ( A  e.  C  ->  ( A Ref B  <->  ( Y  =  X  /\  A. x  e.  A  E. y  e.  B  x  C_  y
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    e. wcel 1819   A.wral 2807   E.wrex 2808   _Vcvv 3109    C_ wss 3471   U.cuni 4251   class class class wbr 4456   Refcref 20129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-xp 5014  df-rel 5015  df-ref 20132
This theorem is referenced by:  refbas  20137  refssex  20138  ssref  20139  refref  20140  reftr  20141  refun0  20142  dissnref  20155  reff  28003  locfinreflem  28004  cmpcref  28014  fnessref  30359  refssfne  30360
  Copyright terms: Public domain W3C validator