elioopnf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elioopnf		Structured version Visualization version GIF version

Theorem elioopnf 13343

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)

**Assertion**
Ref	Expression
elioopnf	⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))

**Proof of Theorem elioopnf**
Step	Hyp	Ref	Expression
1		pnfxr 11166	. . 3 ⊢ +∞ ∈ ℝ^*
2		elioo2 13286	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
4		df-3an 1088	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝐵 < +∞))
5		ltpnf 13019	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
6	5	adantr 480	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 < +∞)
7	6	pm4.71i 559	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝐵 < +∞))
8	4, 7	bitr4i 278	. 2 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
9	3, 8	bitrdi 287	1 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2111 class class class wbr 5089 (class class class)co 7346 ℝcr 11005 +∞cpnf 11143 ℝ^*cxr 11145 < clt 11146 (,)cioo 13245

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-pre-lttri 11080 ax-pre-lttrn 11081

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-po 5522 df-so 5523 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-oprab 7350 df-mpo 7351 df-1st 7921 df-2nd 7922 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-ioo 13249

This theorem is referenced by: mbfmulc2lem 25575 mbfposr 25580 ismbf3d 25582 mbfaddlem 25588 mbfsup 25592 itg2gt0 25688 itg2cnlem1 25689 itg2cnlem2 25690 lhop2 25947 dvfsumlem2 25960 dvfsumlem2OLD 25961 dvfsumlem3 25962 dvfsumrlimge0 25964 dvfsumrlim 25965 dvfsumrlim2 25966 pntpbnd1a 27523 pntpbnd2 27525 pntibndlem2 27529 pntibndlem3 27530 pntlemi 27542 pntlemo 27545 relowlssretop 37407 itg2addnclem2 37722 iblabsnclem 37733 ftc1anclem1 37743 ftc1anclem6 37748 rfcnpre1 45126 regt1loggt0 48647 rege1logbrege0 48669 rege1logbzge0 48670 io1ii 49031

W3C validator