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

Theorem supcl 7818
Description: A supremum belongs to its base class (closure law). See also supub 7819 and suplub 7820. (Contributed by NM, 12-Oct-2004.)
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
supcl  |-  ( ph  ->  sup ( B ,  A ,  R )  e.  A )
Distinct variable groups:    x, y,
z, A    x, R, y, z    x, B, y, z
Allowed substitution hints:    ph( x, y, z)

Proof of Theorem supcl
StepHypRef Expression
1 supmo.1 . . 3  |-  ( ph  ->  R  Or  A )
21supval2 7815 . 2  |-  ( 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 ) ) ) )
3 supcl.2 . . . 4  |-  ( 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 ) ) )
41, 3supeu 7814 . . 3  |-  ( 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 ) ) )
5 riotacl 6175 . . 3  |-  ( 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.  A )
64, 5syl 16 . 2  |-  ( 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.  A )
72, 6eqeltrd 2542 1  |-  ( ph  ->  sup ( B ,  A ,  R )  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1758   A.wral 2798   E.wrex 2799   E!wreu 2800   class class class wbr 4399    Or wor 4747   iota_crio 6159   supcsup 7800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-po 4748  df-so 4749  df-iota 5488  df-riota 6160  df-sup 7801
This theorem is referenced by:  suplub2  7821  supmax  7825  supiso  7832  suprcl  10400  infmsup  10418  supxrcl  11387  infmxrcl  11389  dgrcl  21833  supssd  26154  xrsupssd  26202  xrge0infssd  26204  oddpwdc  26880  wzel  27904  wsuccl  27907  supclt  28779
  Copyright terms: Public domain W3C validator