mnfltt - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem mnfltt 5555

Description: Minus infinity is less than any (finite) real.

**Assertion**
Ref	Expression
mnfltt

**Proof of Theorem mnfltt**
Step	Hyp	Ref	Expression
1		eqid 1478	. . . 4
2	1	jctl 290	. . 3 $/\$
3		olc 268	. . 3 $/\$ $/\$ $\/$ $/\$
4		olc 268	. . 3 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5	2, 3, 4	3syl 20	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
6		rexrt 5511	. . 3
7		mnfxr 5506	. . . 4
8		ltxrt 5507	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	7, 8	mpan 697	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10	6, 9	syl 10	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
11	5, 10	mpbird 196	1

Colors of variables: wff set class

Syntax hints:

wi 3

wb 146 $\/$ wo 222 $/\$ wa 223

wceq 958

wcel 960 class class class wbr 2624

cr 5245

cltrr 5250

cpnf 5495

cmnf 5496

cxr 5497

clt 5498

This theorem is referenced by: mnfltxrt 5557 xrlttrit 5564 xrlttrt 5565 xrrebndt 5580 xrsupsslem 6078 xrub 6082 supxrre 6085 qbtwnxr 6280 elioc2t 6391 elico2t 6392 elicc2t 6393 ioomax 6394 cdrci 10480

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-v 1815 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-qs 4272 df-ni 5012 df-nq 5050 df-np 5098 df-nr 5179 df-c 5252 df-pnf 5499 df-mnf 5500 df-xr 5501 df-ltxr 5502