mnflt - Intuitionistic Logic Explorer

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

Theorem mnflt 9905

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 2205	. . . 4
2		olc 713	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan 424	. . 3 $/\$ $\/$ $/\$
4	3	olcd 736	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		mnfxr 8129	. . 3
6		rexr 8118	. . 3
7		ltxr 9897	. . 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 710

wceq 1373

wcel 2176 class class class wbr 4044

cr 7924

cltrr 7929

cpnf 8104

cmnf 8105

cxr 8106

clt 8107

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-cnex 8016

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-br 4045 df-opab 4106 df-xp 4681 df-pnf 8109 df-mnf 8110 df-xr 8111 df-ltxr 8112

This theorem is referenced by: mnflt0 9906 mnfltxr 9908 xrlttr 9917 xrltso 9918 xrlttri3 9919 ngtmnft 9939 nmnfgt 9940 xrrebnd 9941 xrre3 9944 xltnegi 9957 xltadd1 9998 xposdif 10004 elico2 10059 elicc2 10060 ioomax 10070 elioomnf 10090 qbtwnxr 10400 tgioo 15026