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 )