ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplubti Unicode version

Theorem suplubti 7012
Description: A supremum is the least upper bound. See also supclti 7010 and supubti 7011. (Contributed by Jim Kingdon, 24-Nov-2021.)
Hypotheses
Ref Expression
supmoti.ti  |-  ( (
ph  /\  ( u  e.  A  /\  v  e.  A ) )  -> 
( u  =  v  <-> 
( -.  u R v  /\  -.  v R u ) ) )
supclti.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
suplubti  |-  ( ph  ->  ( ( C  e.  A  /\  C R sup ( B ,  A ,  R )
)  ->  E. z  e.  B  C R
z ) )
Distinct variable groups:    u, A, v, x    y, A, x, z    x, B, y, z    u, R, v, x    y, R, z    ph, u, v, x    z, C
Allowed substitution hints:    ph( y, z)    B( v, u)    C( x, y, v, u)

Proof of Theorem suplubti
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . . . 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.  A  ( y R x  ->  E. z  e.  B  y R z ) )
2 breq1 4018 . . . . . . . 8  |-  ( y  =  w  ->  (
y R x  <->  w R x ) )
3 breq1 4018 . . . . . . . . 9  |-  ( y  =  w  ->  (
y R z  <->  w R
z ) )
43rexbidv 2488 . . . . . . . 8  |-  ( y  =  w  ->  ( E. z  e.  B  y R z  <->  E. z  e.  B  w R
z ) )
52, 4imbi12d 234 . . . . . . 7  |-  ( y  =  w  ->  (
( y R x  ->  E. z  e.  B  y R z )  <->  ( w R x  ->  E. z  e.  B  w R
z ) ) )
65cbvralv 2715 . . . . . 6  |-  ( A. y  e.  A  (
y R x  ->  E. z  e.  B  y R z )  <->  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R
z ) )
71, 6sylib 122 . . . . 5  |-  ( ( A. y  e.  B  -.  x R y  /\  A. y  e.  A  ( y R x  ->  E. z  e.  B  y R z ) )  ->  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R z ) )
87a1i 9 . . . 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 ) )  ->  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R z ) ) )
98ss2rabi 3249 . . 3  |-  { 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. w  e.  A  (
w R x  ->  E. z  e.  B  w R z ) }
10 supmoti.ti . . . . 5  |-  ( (
ph  /\  ( u  e.  A  /\  v  e.  A ) )  -> 
( u  =  v  <-> 
( -.  u R v  /\  -.  v R u ) ) )
11 supclti.2 . . . . 5  |-  ( 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 ) ) )
1210, 11supval2ti 7007 . . . 4  |-  ( 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 ) ) ) )
1310, 11supeuti 7006 . . . . 5  |-  ( 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 ) ) )
14 riotacl2 5857 . . . . 5  |-  ( 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 ) ) } )
1513, 14syl 14 . . . 4  |-  ( 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 ) ) } )
1612, 15eqeltrd 2264 . . 3  |-  ( 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 ) ) } )
179, 16sselid 3165 . 2  |-  ( ph  ->  sup ( B ,  A ,  R )  e.  { x  e.  A  |  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R z ) } )
18 breq2 4019 . . . . . 6  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( w R x  <->  w R sup ( B ,  A ,  R ) ) )
1918imbi1d 231 . . . . 5  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( (
w R x  ->  E. z  e.  B  w R z )  <->  ( w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R z ) ) )
2019ralbidv 2487 . . . 4  |-  ( x  =  sup ( B ,  A ,  R
)  ->  ( A. w  e.  A  (
w R x  ->  E. z  e.  B  w R z )  <->  A. w  e.  A  ( w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R z ) ) )
2120elrab 2905 . . 3  |-  ( sup ( B ,  A ,  R )  e.  {
x  e.  A  |  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R z ) }  <-> 
( sup ( B ,  A ,  R
)  e.  A  /\  A. w  e.  A  ( w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R
z ) ) )
2221simprbi 275 . 2  |-  ( sup ( B ,  A ,  R )  e.  {
x  e.  A  |  A. w  e.  A  ( w R x  ->  E. z  e.  B  w R z ) }  ->  A. w  e.  A  ( w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R
z ) )
23 breq1 4018 . . . . 5  |-  ( w  =  C  ->  (
w R sup ( B ,  A ,  R )  <->  C R sup ( B ,  A ,  R ) ) )
24 breq1 4018 . . . . . 6  |-  ( w  =  C  ->  (
w R z  <->  C R
z ) )
2524rexbidv 2488 . . . . 5  |-  ( w  =  C  ->  ( E. z  e.  B  w R z  <->  E. z  e.  B  C R
z ) )
2623, 25imbi12d 234 . . . 4  |-  ( w  =  C  ->  (
( w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R
z )  <->  ( C R sup ( B ,  A ,  R )  ->  E. z  e.  B  C R z ) ) )
2726rspccv 2850 . . 3  |-  ( A. w  e.  A  (
w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R
z )  ->  ( C  e.  A  ->  ( C R sup ( B ,  A ,  R )  ->  E. z  e.  B  C R
z ) ) )
2827impd 254 . 2  |-  ( A. w  e.  A  (
w R sup ( B ,  A ,  R )  ->  E. z  e.  B  w R
z )  ->  (
( C  e.  A  /\  C R sup ( B ,  A ,  R ) )  ->  E. z  e.  B  C R z ) )
2917, 22, 283syl 17 1  |-  ( ph  ->  ( ( C  e.  A  /\  C R sup ( B ,  A ,  R )
)  ->  E. z  e.  B  C R
z ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1363    e. wcel 2158   A.wral 2465   E.wrex 2466   E!wreu 2467   {crab 2469   class class class wbr 4015   iota_crio 5843   supcsup 6994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-un 3145  df-in 3147  df-ss 3154  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-riota 5844  df-sup 6996
This theorem is referenced by:  suplub2ti  7013  supisoti  7022  infglbti  7037  sup3exmid  8927  maxleast  11235
  Copyright terms: Public domain W3C validator