mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8078

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 8059	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8075	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4213	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2266	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3726	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3328	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8060	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2269	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2164 Vcvv 2760 ∪ cun 3152 𝒫 cpw 3602 {cpr 3620 ℝcr 7873 +∞cpnf 8053 -∞cmnf 8054 ℝ^*cxr 8055

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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4148 ax-pow 4204 ax-un 4465 ax-cnex 7965

This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-rex 2478 df-v 2762 df-un 3158 df-in 3160 df-ss 3167 df-pw 3604 df-sn 3625 df-pr 3626 df-uni 3837 df-pnf 8058 df-mnf 8059 df-xr 8060

This theorem is referenced by: elxr 9845 xrltnr 9848 mnflt 9852 mnfltpnf 9854 nltmnf 9857 mnfle 9861 xrltnsym 9862 xrlttri3 9866 ngtmnft 9886 xrrebnd 9888 xrre2 9890 xrre3 9891 ge0gtmnf 9892 xnegcl 9901 xltnegi 9904 xaddf 9913 xaddval 9914 xaddmnf1 9917 xaddmnf2 9918 pnfaddmnf 9919 mnfaddpnf 9920 xrex 9925 xltadd1 9945 xlt2add 9949 xsubge0 9950 xposdif 9951 xleaddadd 9956 elioc2 10005 elico2 10006 elicc2 10007 ioomax 10017 iccmax 10018 elioomnf 10037 unirnioo 10042 xrmaxadd 11407 reopnap 14725 blssioo 14732 tgioo 14733

W3C validator