Theorem topnfbey

Description: Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020) (Revised by Thierry Arnoux, 2-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	topnfbey	$$⊢B\in \left(0\dots \mathrm{+\infty }\right)\to \mathrm{+\infty }<B$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg B\in \varnothing$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		xrltnr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}\to \neg \mathrm{+\infty }<\mathrm{+\infty }$$
4	2 3	ax-mp	$$⊢\neg \mathrm{+\infty }<\mathrm{+\infty }$$
5		zre	$$⊢\mathrm{+\infty }\in \mathbb{Z}\to \mathrm{+\infty }\in ℝ$$
6		ltpnf	$$⊢\mathrm{+\infty }\in ℝ\to \mathrm{+\infty }<\mathrm{+\infty }$$
7	5 6	syl	$$⊢\mathrm{+\infty }\in \mathbb{Z}\to \mathrm{+\infty }<\mathrm{+\infty }$$
8	4 7	mto	$$⊢\neg \mathrm{+\infty }\in \mathbb{Z}$$
9	8	intnan	$$⊢\neg \left(0\in \mathbb{Z}\wedge \mathrm{+\infty }\in \mathbb{Z}\right)$$
10		fzf	$$⊢\dots :\mathbb{Z}\times \mathbb{Z}⟶𝒫\mathbb{Z}$$
11	10	fdmi	$$⊢\mathrm{dom}\dots =\mathbb{Z}\times \mathbb{Z}$$
12	11	ndmov	$$⊢\neg \left(0\in \mathbb{Z}\wedge \mathrm{+\infty }\in \mathbb{Z}\right)\to \left(0\dots \mathrm{+\infty }\right)=\varnothing$$
13	9 12	ax-mp	$$⊢\left(0\dots \mathrm{+\infty }\right)=\varnothing$$
14	13	eleq2i	$$⊢B\in \left(0\dots \mathrm{+\infty }\right)\leftrightarrow B\in \varnothing$$
15	1 14	mtbir	$$⊢\neg B\in \left(0\dots \mathrm{+\infty }\right)$$
16	15	pm2.21i	$$⊢B\in \left(0\dots \mathrm{+\infty }\right)\to \mathrm{+\infty }<B$$