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	⊢ ( 𝐵 ∈ ( 0 ... +∞ ) → +∞ < 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝐵 ∈ ∅
2		pnfxr	⊢ +∞ ∈ ℝ*
3		xrltnr	⊢ ( +∞ ∈ ℝ* → ¬ +∞ < +∞ )
4	2 3	ax-mp	⊢ ¬ +∞ < +∞
5		zre	⊢ ( +∞ ∈ ℤ → +∞ ∈ ℝ )
6		ltpnf	⊢ ( +∞ ∈ ℝ → +∞ < +∞ )
7	5 6	syl	⊢ ( +∞ ∈ ℤ → +∞ < +∞ )
8	4 7	mto	⊢ ¬ +∞ ∈ ℤ
9	8	intnan	⊢ ¬ ( 0 ∈ ℤ ∧ +∞ ∈ ℤ )
10		fzf	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
11	10	fdmi	⊢ dom ... = ( ℤ × ℤ )
12	11	ndmov	⊢ ( ¬ ( 0 ∈ ℤ ∧ +∞ ∈ ℤ ) → ( 0 ... +∞ ) = ∅ )
13	9 12	ax-mp	⊢ ( 0 ... +∞ ) = ∅
14	13	eleq2i	⊢ ( 𝐵 ∈ ( 0 ... +∞ ) ↔ 𝐵 ∈ ∅ )
15	1 14	mtbir	⊢ ¬ 𝐵 ∈ ( 0 ... +∞ )
16	15	pm2.21i	⊢ ( 𝐵 ∈ ( 0 ... +∞ ) → +∞ < 𝐵 )