Metamath Proof Explorer

Definition df-bj-pinfty

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

Ref Expression
Assertion df-bj-pinfty 
|- pinfty = ( inftyexpi ` 0 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpinfty 
 |-  pinfty
1 cinftyexpi 
 |-  inftyexpi
2 cc0 
 |-  0
3 2 1 cfv 
 |-  ( inftyexpi ` 0 )
4 0 3 wceq 
 |-  pinfty = ( inftyexpi ` 0 )