mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8136

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 8117	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8133	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4231	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2279	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3741	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3342	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8118	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2282	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2177 Vcvv 2773 ∪ cun 3165 𝒫 cpw 3617 {cpr 3635 ℝcr 7931 +∞cpnf 8111 -∞cmnf 8112 ℝ^*cxr 8113

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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4166 ax-pow 4222 ax-un 4484 ax-cnex 8023

This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-rex 2491 df-v 2775 df-un 3171 df-in 3173 df-ss 3180 df-pw 3619 df-sn 3640 df-pr 3641 df-uni 3853 df-pnf 8116 df-mnf 8117 df-xr 8118

This theorem is referenced by: elxr 9905 xrltnr 9908 mnflt 9912 mnfltpnf 9914 nltmnf 9917 mnfle 9921 xrltnsym 9922 xrlttri3 9926 ngtmnft 9946 xrrebnd 9948 xrre2 9950 xrre3 9951 ge0gtmnf 9952 xnegcl 9961 xltnegi 9964 xaddf 9973 xaddval 9974 xaddmnf1 9977 xaddmnf2 9978 pnfaddmnf 9979 mnfaddpnf 9980 xrex 9985 xltadd1 10005 xlt2add 10009 xsubge0 10010 xposdif 10011 xleaddadd 10016 elioc2 10065 elico2 10066 elicc2 10067 ioomax 10077 iccmax 10078 elioomnf 10097 unirnioo 10102 xrmaxadd 11616 reopnap 15062 blssioo 15069 tgioo 15070

W3C validator