Metamath Proof Explorer

Definition df-bj-minfty

Description: Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion df-bj-minfty 
|- minfty = ( inftyexpi ` _pi )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminfty 
 |-  minfty
1 cinftyexpi 
 |-  inftyexpi
2 cpi 
 |-  _pi
3 2 1 cfv 
 |-  ( inftyexpi ` _pi )
4 0 3 wceq 
 |-  minfty = ( inftyexpi ` _pi )