![]() |
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 7622 |
. . . . 5
![]() ![]() ![]() ![]() ![]() | |
2 | pnfex 7638 |
. . . . . 6
![]() ![]() ![]() ![]() | |
3 | 2 | pwex 4039 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eqeltri 2167 |
. . . 4
![]() ![]() ![]() ![]() |
5 | 4 | prid2 3569 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | elun2 3183 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | ax-mp 7 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-xr 7623 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | eleqtrri 2170 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-un 4284 ax-cnex 7533 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rex 2376 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-uni 3676 df-pnf 7621 df-mnf 7622 df-xr 7623 |
This theorem is referenced by: elxr 9346 xrltnr 9349 mnflt 9352 mnfltpnf 9354 nltmnf 9357 mnfle 9361 xrltnsym 9362 xrlttri3 9366 ngtmnft 9383 xrrebnd 9385 xrre2 9387 xrre3 9388 ge0gtmnf 9389 xnegcl 9398 xltnegi 9401 xaddf 9410 xaddval 9411 xaddmnf1 9414 xaddmnf2 9415 pnfaddmnf 9416 mnfaddpnf 9417 xrex 9422 xltadd1 9442 xlt2add 9446 xsubge0 9447 xposdif 9448 xleaddadd 9453 elioc2 9502 elico2 9503 elicc2 9504 ioomax 9514 iccmax 9515 elioomnf 9534 unirnioo 9539 xrmaxadd 10820 blssioo 12335 tgioo 12336 |
Copyright terms: Public domain | W3C validator |