mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 7976

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 7957	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 7973	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4169	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2243	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3690	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3295	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 7958	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2246	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2141 Vcvv 2730 ∪ cun 3119 𝒫 cpw 3566 {cpr 3584 ℝcr 7773 +∞cpnf 7951 -∞cmnf 7952 ℝ^*cxr 7953

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-un 4418 ax-cnex 7865

This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rex 2454 df-v 2732 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-uni 3797 df-pnf 7956 df-mnf 7957 df-xr 7958

This theorem is referenced by: elxr 9733 xrltnr 9736 mnflt 9740 mnfltpnf 9742 nltmnf 9745 mnfle 9749 xrltnsym 9750 xrlttri3 9754 ngtmnft 9774 xrrebnd 9776 xrre2 9778 xrre3 9779 ge0gtmnf 9780 xnegcl 9789 xltnegi 9792 xaddf 9801 xaddval 9802 xaddmnf1 9805 xaddmnf2 9806 pnfaddmnf 9807 mnfaddpnf 9808 xrex 9813 xltadd1 9833 xlt2add 9837 xsubge0 9838 xposdif 9839 xleaddadd 9844 elioc2 9893 elico2 9894 elicc2 9895 ioomax 9905 iccmax 9906 elioomnf 9925 unirnioo 9930 xrmaxadd 11224 reopnap 13332 blssioo 13339 tgioo 13340

W3C validator