Metamath Proof Explorer

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 e. ( 0 ... +oo ) -> +oo < B )

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. B e. (/)
2 pnfxr 
 |-  +oo e. RR*
3 xrltnr 
 |-  ( +oo e. RR* -> -. +oo < +oo )
4 2 3 ax-mp 
 |-  -. +oo < +oo
5 zre 
 |-  ( +oo e. ZZ -> +oo e. RR )
6 ltpnf 
 |-  ( +oo e. RR -> +oo < +oo )
7 5 6 syl 
 |-  ( +oo e. ZZ -> +oo < +oo )
8 4 7 mto 
 |-  -. +oo e. ZZ
9 8 intnan 
 |-  -. ( 0 e. ZZ /\ +oo e. ZZ )
10 fzf 
 |-  ... : ( ZZ X. ZZ ) --> ~P ZZ
11 10 fdmi 
 |-  dom ... = ( ZZ X. ZZ )
12 11 ndmov 
 |-  ( -. ( 0 e. ZZ /\ +oo e. ZZ ) -> ( 0 ... +oo ) = (/) )
13 9 12 ax-mp 
 |-  ( 0 ... +oo ) = (/)
14 13 eleq2i 
 |-  ( B e. ( 0 ... +oo ) <-> B e. (/) )
15 1 14 mtbir 
 |-  -. B e. ( 0 ... +oo )
16 15 pm2.21i 
 |-  ( B e. ( 0 ... +oo ) -> +oo < B )