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

Definition df-infp 25738
Description: Definition of the infimum of an indexed class of extended reals. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-infp  |-  inf _  x  e.  A B  =  (  <_  inf w  ( ( x  e.  A  |->  B ) " A ) )

Detailed syntax breakdown of Definition df-infp
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3clinfp 25736 . 2  class  inf _  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 cinf 14320 . . 3  class  inf w
95, 7, 8co 5874 . 2  class  (  <_  inf w  ( ( x  e.  A  |->  B )
" A ) )
104, 9wceq 1632 1  wff  inf _  x  e.  A B  =  (  <_  inf w  ( ( x  e.  A  |->  B ) " A ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator