mnfltpnf - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem mnfltpnf 6719

Description: Minus infinity is less than plus infinity.

**Assertion**
Ref	Expression
mnfltpnf

**Proof of Theorem mnfltpnf**
Step	Hyp	Ref	Expression
1		eqid 1884	. . . 4
2		eqid 1884	. . . 4
3		olc 290	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
4	1, 2, 3	mp2an 761	. . 3 $/\$ $/\$ $\/$ $/\$
5	4	orci 292	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
6		mnfxr 6662	. . 3
7		pnfxr 6660	. . 3
8		ltxr 6664	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	6, 7, 8	mp2an 761	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10	5, 9	mpbir 207	1

Colors of variables: wff set class

Syntax hints:

wb 163 $\/$ wo 239 $/\$ wa 240

wceq 1298

wcel 1300 class class class wbr 3338

cr 6385

cltrr 6390

cpnf 6650

cmnf 6651

cxr 6652

clt 6653

This theorem is referenced by: mnfltxr 6720 xrlttri 6727 xrlttr 6728

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-qs 5323 df-ni 6152 df-nq 6190 df-np 6238 df-nr 6319 df-c 6392 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657