HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
Description: Plus and minus infinity
are distinguished elements of  . |
| Ref | Expression |
|---|---|
| pnfnemnf |
    |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pnfxr 5647 |
. . . 4
 | |
| 2 | pwne 4633 |
. . . 4
 
 | |
| 3 | 1, 2 | ax-mp 7 |
. . 3
|
| 4 | necom 1682 |
. . 3
 | |
| 5 | 3, 4 | mpbir 188 |
. 2
|
| 6 | df-mnf 5642 |
. . 3
 | |
| 7 | 6 | neeq2i 1636 |
. 2
|
| 8 | 5, 7 | mpbir 188 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wcel 994 wne 1628 cpw 2458 cpnf 5637 cmnf 5638 cxr 5639 |
| This theorem is referenced by: xrltnr 5695 pnfnlt 5700 nltmnf 5701 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089 ax-inf2 4770 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-rab 1698 df-v 1858 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-qs 4406 df-en 4509 df-dom 4510 df-sdom 4511 df-ni 5154 df-nq 5192 df-np 5240 df-nr 5321 df-c 5394 df-pnf 5641 df-mnf 5642 df-xr 5643 |