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 13450

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 11282	. . 3 ⊢ +∞ ∈ ℝ^*
2		elioo2 13395	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞)))
4		df-3an 1088	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝐵 < +∞))
5		ltpnf 13129	. . . . 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 2107 class class class wbr 5117 (class class class)co 7400 ℝcr 11121 +∞cpnf 11259 ℝ^*cxr 11261 < clt 11262 (,)cioo 13354

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-sep 5264 ax-nul 5274 ax-pow 5333 ax-pr 5400 ax-un 7724 ax-cnex 11178 ax-resscn 11179 ax-pre-lttri 11196 ax-pre-lttrn 11197

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rab 3414 df-v 3459 df-sbc 3764 df-csb 3873 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-op 4606 df-uni 4882 df-iun 4967 df-br 5118 df-opab 5180 df-mpt 5200 df-id 5546 df-po 5559 df-so 5560 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-ov 7403 df-oprab 7404 df-mpo 7405 df-1st 7983 df-2nd 7984 df-er 8714 df-en 8955 df-dom 8956 df-sdom 8957 df-pnf 11264 df-mnf 11265 df-xr 11266 df-ltxr 11267 df-le 11268 df-ioo 13358

This theorem is referenced by: mbfmulc2lem 25587 mbfposr 25592 ismbf3d 25594 mbfaddlem 25600 mbfsup 25604 itg2gt0 25700 itg2cnlem1 25701 itg2cnlem2 25702 lhop2 25959 dvfsumlem2 25972 dvfsumlem2OLD 25973 dvfsumlem3 25974 dvfsumrlimge0 25976 dvfsumrlim 25977 dvfsumrlim2 25978 pntpbnd1a 27534 pntpbnd2 27536 pntibndlem2 27540 pntibndlem3 27541 pntlemi 27553 pntlemo 27556 relowlssretop 37310 itg2addnclem2 37625 iblabsnclem 37636 ftc1anclem1 37646 ftc1anclem6 37651 rfcnpre1 44977 regt1loggt0 48410 rege1logbrege0 48432 rege1logbzge0 48433 io1ii 48789

W3C validator