mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8171

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.)

**Assertion**
Ref	Expression
mnfxr	⊢ -∞ ∈ ℝ^*

**Proof of Theorem mnfxr**
Step	Hyp	Ref	Expression
1		df-mnf 8152	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8168	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4246	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2282	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3753	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3352	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8153	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2285	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2180 Vcvv 2779 ∪ cun 3175 𝒫 cpw 3629 {cpr 3647 ℝcr 7966 +∞cpnf 8146 -∞cmnf 8147 ℝ^*cxr 8148

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 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-sep 4181 ax-pow 4237 ax-un 4501 ax-cnex 8058

This theorem depends on definitions: df-bi 117 df-tru 1378 df-nf 1487 df-sb 1789 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-rex 2494 df-v 2781 df-un 3181 df-in 3183 df-ss 3190 df-pw 3631 df-sn 3652 df-pr 3653 df-uni 3868 df-pnf 8151 df-mnf 8152 df-xr 8153

This theorem is referenced by: elxr 9940 xrltnr 9943 mnflt 9947 mnfltpnf 9949 nltmnf 9952 mnfle 9956 xrltnsym 9957 xrlttri3 9961 ngtmnft 9981 xrrebnd 9983 xrre2 9985 xrre3 9986 ge0gtmnf 9987 xnegcl 9996 xltnegi 9999 xaddf 10008 xaddval 10009 xaddmnf1 10012 xaddmnf2 10013 pnfaddmnf 10014 mnfaddpnf 10015 xrex 10020 xltadd1 10040 xlt2add 10044 xsubge0 10045 xposdif 10046 xleaddadd 10051 elioc2 10100 elico2 10101 elicc2 10102 ioomax 10112 iccmax 10113 elioomnf 10132 unirnioo 10137 xrmaxadd 11738 reopnap 15185 blssioo 15192 tgioo 15193

W3C validator