mnfltpnf - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem mnfltpnf 5517

Description: Minus infinity is less than plus infinity.

**Assertion**
Ref	Expression
mnfltpnf

**Proof of Theorem mnfltpnf**
Step	Hyp	Ref	Expression
1		eqid 1468	. . . 4
2		eqid 1468	. . . 4
3		olc 268	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
4	1, 2, 3	mp2an 695	. . 3 $/\$ $/\$ $\/$ $/\$
5	4	orci 270	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
6		mnfxr 5466	. . 3
7		pnfxr 5465	. . 3
8		ltxrt 5467	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	6, 7, 8	mp2an 695	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10	5, 9	mpbir 190	1

Colors of variables: wff set class

Syntax hints:

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

wceq 953

wcel 955 class class class wbr 2609

cr 5205

cltrr 5210

cpnf 5455

cmnf 5456

cxr 5457

clt 5458

This theorem is referenced by: mnfltxrt 5518 xrlttrit 5525 xrlttrt 5526

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-qs 4250 df-ni 4972 df-nq 5010 df-np 5058 df-nr 5139 df-c 5212 df-pnf 5459 df-mnf 5460 df-xr 5461 df-ltxr 5462