mnflt - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mnflt		Unicode version

Theorem mnflt 9797

Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
mnflt

**Proof of Theorem mnflt**
Step	Hyp	Ref	Expression
1		eqid 2187	. . . 4
2		olc 712	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan 424	. . 3 $/\$ $\/$ $/\$
4	3	olcd 735	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		mnfxr 8028	. . 3
6		rexr 8017	. . 3
7		ltxr 9789	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
8	5, 6, 7	sylancr 414	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	4, 8	mpbird 167	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709

wceq 1363

wcel 2158 class class class wbr 4015

cr 7824

cltrr 7829

cpnf 8003

cmnf 8004

cxr 8005

clt 8006

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-cnex 7916

This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-br 4016 df-opab 4077 df-xp 4644 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011

This theorem is referenced by: mnflt0 9798 mnfltxr 9800 xrlttr 9809 xrltso 9810 xrlttri3 9811 ngtmnft 9831 nmnfgt 9832 xrrebnd 9833 xrre3 9836 xltnegi 9849 xltadd1 9890 xposdif 9896 elico2 9951 elicc2 9952 ioomax 9962 elioomnf 9982 qbtwnxr 10272 tgioo 14342