mnflt - Intuitionistic Logic Explorer

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

Theorem mnflt 9907

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 8131	. . 3
6		rexr 8120	. . 3
7		ltxr 9899	. . 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 4045

cr 7926

cltrr 7931

cpnf 8106

cmnf 8107

cxr 8108

clt 8109

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 4163 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-cnex 8018

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 4046 df-opab 4107 df-xp 4682 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114

This theorem is referenced by: mnflt0 9908 mnfltxr 9910 xrlttr 9919 xrltso 9920 xrlttri3 9921 ngtmnft 9941 nmnfgt 9942 xrrebnd 9943 xrre3 9946 xltnegi 9959 xltadd1 10000 xposdif 10006 elico2 10061 elicc2 10062 ioomax 10072 elioomnf 10092 qbtwnxr 10402 tgioo 15059