Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mnfxr | Unicode version |
Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Ref | Expression |
---|---|
mnfxr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mnf 7796 | . . . . 5 | |
2 | pnfex 7812 | . . . . . 6 | |
3 | 2 | pwex 4102 | . . . . 5 |
4 | 1, 3 | eqeltri 2210 | . . . 4 |
5 | 4 | prid2 3625 | . . 3 |
6 | elun2 3239 | . . 3 | |
7 | 5, 6 | ax-mp 5 | . 2 |
8 | df-xr 7797 | . 2 | |
9 | 7, 8 | eleqtrri 2213 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 cvv 2681 cun 3064 cpw 3505 cpr 3523 cr 7612 cpnf 7790 cmnf 7791 cxr 7792 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-sep 4041 ax-pow 4093 ax-un 4350 ax-cnex 7704 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-rex 2420 df-v 2683 df-un 3070 df-in 3072 df-ss 3079 df-pw 3507 df-sn 3528 df-pr 3529 df-uni 3732 df-pnf 7795 df-mnf 7796 df-xr 7797 |
This theorem is referenced by: elxr 9556 xrltnr 9559 mnflt 9562 mnfltpnf 9564 nltmnf 9567 mnfle 9571 xrltnsym 9572 xrlttri3 9576 ngtmnft 9593 xrrebnd 9595 xrre2 9597 xrre3 9598 ge0gtmnf 9599 xnegcl 9608 xltnegi 9611 xaddf 9620 xaddval 9621 xaddmnf1 9624 xaddmnf2 9625 pnfaddmnf 9626 mnfaddpnf 9627 xrex 9632 xltadd1 9652 xlt2add 9656 xsubge0 9657 xposdif 9658 xleaddadd 9663 elioc2 9712 elico2 9713 elicc2 9714 ioomax 9724 iccmax 9725 elioomnf 9744 unirnioo 9749 xrmaxadd 11023 reopnap 12696 blssioo 12703 tgioo 12704 |
Copyright terms: Public domain | W3C validator |