MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-spw Unicode version

Definition df-spw 14308
Description: Define suprema under weak orderings. Unlike df-sup 7194 for strong orderings,  sup w is evaluates to a member of the field of  R iff the supremum exists. Read 
R  sup w  A as the  R-supremum of set  A. (Contributed by NM, 13-May-2008.)
Assertion
Ref Expression
df-spw  |-  sup w  =  ( r  e.  PosetRel
,  x  e.  _V  |->  ( iota_ y  e.  U. U. r ( A. z  e.  x  z r
y  /\  A. z  e.  U. U. r ( A. w  e.  x  w r z  -> 
y r z ) ) ) )
Distinct variable group:    x, r, y, z, w

Detailed syntax breakdown of Definition df-spw
StepHypRef Expression
1 cspw 14303 . 2  class  sup w
2 vr . . 3  set  r
3 vx . . 3  set  x
4 cps 14301 . . 3  class  PosetRel
5 cvv 2788 . . 3  class  _V
6 vz . . . . . . . 8  set  z
76cv 1622 . . . . . . 7  class  z
8 vy . . . . . . . 8  set  y
98cv 1622 . . . . . . 7  class  y
102cv 1622 . . . . . . 7  class  r
117, 9, 10wbr 4023 . . . . . 6  wff  z r y
123cv 1622 . . . . . 6  class  x
1311, 6, 12wral 2543 . . . . 5  wff  A. z  e.  x  z r
y
14 vw . . . . . . . . . 10  set  w
1514cv 1622 . . . . . . . . 9  class  w
1615, 7, 10wbr 4023 . . . . . . . 8  wff  w r z
1716, 14, 12wral 2543 . . . . . . 7  wff  A. w  e.  x  w r
z
189, 7, 10wbr 4023 . . . . . . 7  wff  y r z
1917, 18wi 4 . . . . . 6  wff  ( A. w  e.  x  w
r z  ->  y
r z )
2010cuni 3827 . . . . . . 7  class  U. r
2120cuni 3827 . . . . . 6  class  U. U. r
2219, 6, 21wral 2543 . . . . 5  wff  A. z  e.  U. U. r ( A. w  e.  x  w r z  -> 
y r z )
2313, 22wa 358 . . . 4  wff  ( A. z  e.  x  z
r y  /\  A. z  e.  U. U. r
( A. w  e.  x  w r z  ->  y r z ) )
2423, 8, 21crio 6297 . . 3  class  ( iota_ y  e.  U. U. r
( A. z  e.  x  z r y  /\  A. z  e. 
U. U. r ( A. w  e.  x  w
r z  ->  y
r z ) ) )
252, 3, 4, 5, 24cmpt2 5860 . 2  class  ( r  e.  PosetRel ,  x  e.  _V  |->  ( iota_ y  e. 
U. U. r ( A. z  e.  x  z
r y  /\  A. z  e.  U. U. r
( A. w  e.  x  w r z  ->  y r z ) ) ) )
261, 25wceq 1623 1  wff  sup w  =  ( r  e.  PosetRel
,  x  e.  _V  |->  ( iota_ y  e.  U. U. r ( A. z  e.  x  z r
y  /\  A. z  e.  U. U. r ( A. w  e.  x  w r z  -> 
y r z ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  spwval2  14333
  Copyright terms: Public domain W3C validator