Theorem infxrre 13318

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 5-Sep-2020.)

Assertion

Ref	Expression
infxrre	⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem infxrre

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1133	. . . 4 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ)
2		ressxr 11259	. . . 4 ⊢ ℝ ⊆ ℝ*
3	1, 2	sstrdi 3989	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ*)
4		infxrcl 13315	. . 3 ⊢ (𝐴 ⊆ ℝ* → inf(𝐴, ℝ*, < ) ∈ ℝ*)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
6		infrecl 12197	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ)
7	6	rexrd 11265	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ*)
8	5	xrleidd 13134	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ))
9		infxrgelb 13317	. . . . 5 ⊢ ((𝐴 ⊆ ℝ* ∧ inf(𝐴, ℝ*, < ) ∈ ℝ*) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
10	3, 5, 9	syl2anc 583	. . . 4 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
11		simp2 1134	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ≠ ∅)
12		n0 4341	. . . . . . 7 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐴)
13	11, 12	sylib 217	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑧 𝑧 ∈ 𝐴)
14	5	adantr 480	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
15	1	sselda 3977	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
16		mnfxr 11272	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ*
17	16	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ ∈ ℝ*)
18	6	mnfltd 13107	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ, < ))
19	6	leidd 11781	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ))
20		infregelb 12199	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ, < ) ∈ ℝ) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
21	6, 20	mpdan 684	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
22		infxrgelb 13317	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ* ∧ inf(𝐴, ℝ, < ) ∈ ℝ*) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
23	3, 7, 22	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
24	21, 23	bitr4d 282	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < )))
25	19, 24	mpbid 231	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ))
26	17, 7, 5, 18, 25	xrltletrd 13143	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ*, < ))
27	26	adantr 480	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → -∞ < inf(𝐴, ℝ*, < ))
28		infxrlb 13316	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ* ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧)
29	3, 28	sylan 579	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧)
30		xrre 13151	. . . . . . 7 ⊢ (((inf(𝐴, ℝ*, < ) ∈ ℝ* ∧ 𝑧 ∈ ℝ) ∧ (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) ≤ 𝑧)) → inf(𝐴, ℝ*, < ) ∈ ℝ)
31	14, 15, 27, 29, 30	syl22anc 836	. . . . . 6 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈ ℝ)
32	13, 31	exlimddv 1930	. . . . 5 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈ ℝ)
33		infregelb 12199	. . . . 5 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
34	32, 33	mpdan 684	. . . 4 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
35	10, 34	bitr4d 282	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < )))
36	8, 35	mpbid 231	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ))
37	5, 7, 36, 25	xrletrid 13137	1 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2934  ∀wral 3055  ∃wrex 3064   ⊆ wss 3943  ∅c0 4317   class class class wbr 5141  infcinf 9435  ℝcr 11108  -∞cmnf 11247  ℝ^*cxr 11248   < clt 11249   ≤ cle 11250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-sup 9436  df-inf 9437  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448

This theorem is referenced by:  mbflimsup  25546  infxrrefi  44645  supminfxr  44727  climinf2lem  44975  limsupvaluz2  45007