Description: Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | df-bj-pinfty | ⊢ +∞ = ( +∞ei ‘ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cpinfty | ⊢ +∞ | |
1 | cinftyexpi | ⊢ +∞ei | |
2 | cc0 | ⊢ 0 | |
3 | 2 1 | cfv | ⊢ ( +∞ei ‘ 0 ) |
4 | 0 3 | wceq | ⊢ +∞ = ( +∞ei ‘ 0 ) |