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

Theorem supub 7931
Description: A supremum is an upper bound. See also supcl 7930 and suplub 7932.

This proof demonstrates how to expand an iota-based definition (df-iota 5557) using riotacl2 6270.

(Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)

Hypotheses
Ref Expression
supmo.1  |-  ( ph  ->  R  Or  A )
supcl.2  |-  ( ph  ->  E. x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) )
Assertion
Ref Expression
supub  |-  ( ph  ->  ( C  e.  B  ->  -.  sup ( B ,  A ,  R
) R C ) )
Distinct variable groups:    x, y,
z, A    x, R, y, z    x, B, y, z
Allowed substitution hints:    ph( x, y, z)    C( x, y, z)

Proof of Theorem supub
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . . . . 6  |-  ( ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) )  ->  A. y  e.  B  -.  x R y )
21a1i 11 . . . . 5  |-  ( x  e.  A  ->  (
( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R
z ) )  ->  A. y  e.  B  -.  x R y ) )
32ss2rabi 3587 . . . 4  |-  { x  e.  A  |  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) }  C_  { x  e.  A  |  A. y  e.  B  -.  x R y }
4 supmo.1 . . . . . 6  |-  ( ph  ->  R  Or  A )
54supval2 7927 . . . . 5  |-  ( ph  ->  sup ( B ,  A ,  R )  =  ( iota_ x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  (
y R x  ->  E. z  e.  B  y R z ) ) ) )
6 supcl.2 . . . . . . 7  |-  ( ph  ->  E. x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) )
74, 6supeu 7926 . . . . . 6  |-  ( ph  ->  E! x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) )
8 riotacl2 6270 . . . . . 6  |-  ( E! x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) )  ->  ( iota_ x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  (
y R x  ->  E. z  e.  B  y R z ) ) )  e.  { x  e.  A  |  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) } )
97, 8syl 16 . . . . 5  |-  ( ph  ->  ( iota_ x  e.  A  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) )  e.  { x  e.  A  |  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) ) } )
105, 9eqeltrd 2555 . . . 4  |-  ( ph  ->  sup ( B ,  A ,  R )  e.  { x  e.  A  |  ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  (
y R x  ->  E. z  e.  B  y R z ) ) } )
113, 10sseldi 3507 . . 3  |-  ( ph  ->  sup ( B ,  A ,  R )  e.  { x  e.  A  |  A. y  e.  B  -.  x R y } )
12 breq2 4457 . . . . . . . 8  |-  ( y  =  w  ->  (
x R y  <->  x R w ) )
1312notbid 294 . . . . . . 7  |-  ( y  =  w  ->  ( -.  x R y  <->  -.  x R w ) )
1413cbvralv 3093 . . . . . 6  |-  ( A. y  e.  B  -.  x R y  <->  A. w  e.  B  -.  x R w )
15 breq1 4456 . . . . . . . 8  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( x R w  <->  sup ( B ,  A ,  R ) R w ) )
1615notbid 294 . . . . . . 7  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( -.  x R w  <->  -.  sup ( B ,  A ,  R ) R w ) )
1716ralbidv 2906 . . . . . 6  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( A. w  e.  B  -.  x R w  <->  A. w  e.  B  -.  sup ( B ,  A ,  R ) R w ) )
1814, 17syl5bb 257 . . . . 5  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( A. y  e.  B  -.  x R y  <->  A. w  e.  B  -.  sup ( B ,  A ,  R ) R w ) )
1918elrab 3266 . . . 4  |-  ( sup ( B ,  A ,  R )  e.  {
x  e.  A  |  A. y  e.  B  -.  x R y }  <-> 
( sup ( B ,  A ,  R
)  e.  A  /\  A. w  e.  B  -.  sup ( B ,  A ,  R ) R w ) )
2019simprbi 464 . . 3  |-  ( sup ( B ,  A ,  R )  e.  {
x  e.  A  |  A. y  e.  B  -.  x R y }  ->  A. w  e.  B  -.  sup ( B ,  A ,  R ) R w )
2111, 20syl 16 . 2  |-  ( ph  ->  A. w  e.  B  -.  sup ( B ,  A ,  R ) R w )
22 breq2 4457 . . . 4  |-  ( w  =  C  ->  ( sup ( B ,  A ,  R ) R w  <->  sup ( B ,  A ,  R ) R C ) )
2322notbid 294 . . 3  |-  ( w  =  C  ->  ( -.  sup ( B ,  A ,  R ) R w  <->  -.  sup ( B ,  A ,  R ) R C ) )
2423rspccv 3216 . 2  |-  ( A. w  e.  B  -.  sup ( B ,  A ,  R ) R w  ->  ( C  e.  B  ->  -.  sup ( B ,  A ,  R ) R C ) )
2521, 24syl 16 1  |-  ( ph  ->  ( C  e.  B  ->  -.  sup ( B ,  A ,  R
) R C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   E!wreu 2819   {crab 2821   class class class wbr 4453    Or wor 4805   iota_crio 6255   supcsup 7912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-po 4806  df-so 4807  df-iota 5557  df-riota 6256  df-sup 7913
This theorem is referenced by:  suplub2  7933  supmax  7937  supgtoreq  7940  supiso  7945  suprub  10516  infmrlb  10536  suprzub  11185  supxrun  11519  supxrub  11528  infmxrlb  11537  dgrub  22499  supssd  27350  ssnnssfz  27420  oddpwdc  28118  ballotlemimin  28269  ballotlemfrcn0  28293  wsuclb  29311  itg2addnclem  29993  supubt  30157  ssnn0ssfz  32417
  Copyright terms: Public domain W3C validator