Metamath Proof Explorer


Definition df-bj-pinfty

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

Ref Expression
Assertion df-bj-pinfty +∞ = ( +∞ei ‘ 0 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpinfty +∞
1 cinftyexpi +∞ei
2 cc0 0
3 2 1 cfv ( +∞ei ‘ 0 )
4 0 3 wceq +∞ = ( +∞ei ‘ 0 )