Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-supp Unicode version

Definition df-supp 25737
Description: Definition of the supremum of an indexed class of extended reals. (Contributed by FL, 16-Apr-2012.)
Assertion
Ref Expression
df-supp  |-  sup _  x  e.  A B  =  (  <_  sup w  ( ( x  e.  A  |->  B ) " A ) )

Detailed syntax breakdown of Definition df-supp
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3clsupp 25735 . 2  class  sup _  x  e.  A B
5 cle 8884 . . 3  class  <_
61, 2, 3cmpt 4093 . . . 4  class  ( x  e.  A  |->  B )
76, 2cima 4708 . . 3  class  ( ( x  e.  A  |->  B ) " A )
8 cspw 14319 . . 3  class  sup w
95, 7, 8co 5874 . 2  class  (  <_  sup w  ( ( x  e.  A  |->  B )
" A ) )
104, 9wceq 1632 1  wff  sup _  x  e.  A B  =  (  <_  sup w  ( ( x  e.  A  |->  B ) " A ) )
Colors of variables: wff set class
This definition is referenced by:  supbrr  25739
  Copyright terms: Public domain W3C validator