Theorem infxrre 13355

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 11296	. . . 4 ⊢ ℝ ⊆ ℝ*
3	1, 2	sstrdi 3994	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ*)
4		infxrcl 13352	. . 3 ⊢ (𝐴 ⊆ ℝ* → inf(𝐴, ℝ*, < ) ∈ ℝ*)
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
6		infrecl 12234	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ)
7	6	rexrd 11302	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ*)
8	5	xrleidd 13171	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ))
9		infxrgelb 13354	. . . . 5 ⊢ ((𝐴 ⊆ ℝ* ∧ inf(𝐴, ℝ*, < ) ∈ ℝ*) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
10	3, 5, 9	syl2anc 582	. . . 4 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
11		simp2 1134	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ≠ ∅)
12		n0 4350	. . . . . . 7 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐴)
13	11, 12	sylib 217	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑧 𝑧 ∈ 𝐴)
14	5	adantr 479	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
15	1	sselda 3982	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
16		mnfxr 11309	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ*
17	16	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ ∈ ℝ*)
18	6	mnfltd 13144	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ, < ))
19	6	leidd 11818	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ))
20		infregelb 12236	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ, < ) ∈ ℝ) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
21	6, 20	mpdan 685	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
22		infxrgelb 13354	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ* ∧ inf(𝐴, ℝ, < ) ∈ ℝ*) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
23	3, 7, 22	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥))
24	21, 23	bitr4d 281	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < )))
25	19, 24	mpbid 231	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ))
26	17, 7, 5, 18, 25	xrltletrd 13180	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ*, < ))
27	26	adantr 479	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → -∞ < inf(𝐴, ℝ*, < ))
28		infxrlb 13353	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ* ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧)
29	3, 28	sylan 578	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧)
30		xrre 13188	. . . . . . 7 ⊢ (((inf(𝐴, ℝ*, < ) ∈ ℝ* ∧ 𝑧 ∈ ℝ) ∧ (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) ≤ 𝑧)) → inf(𝐴, ℝ*, < ) ∈ ℝ)
31	14, 15, 27, 29, 30	syl22anc 837	. . . . . 6 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈ ℝ)
32	13, 31	exlimddv 1930	. . . . 5 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈ ℝ)
33		infregelb 12236	. . . . 5 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
34	32, 33	mpdan 685	. . . 4 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥))
35	10, 34	bitr4d 281	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ) ↔ inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < )))
36	8, 35	mpbid 231	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ))
37	5, 7, 36, 25	xrletrid 13174	1 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2937  ∀wral 3058  ∃wrex 3067   ⊆ wss 3949  ∅c0 4326   class class class wbr 5152  infcinf 9472  ℝcr 11145  -∞cmnf 11284  ℝ^*cxr 11285   < clt 11286   ≤ cle 11287

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 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485

This theorem is referenced by:  mbflimsup  25615  infxrrefi  44793  supminfxr  44875  climinf2lem  45123  limsupvaluz2  45155