infxrgelb - Metamath Proof Explorer

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

Theorem infxrgelb 13357

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.)

**Assertion**
Ref	Expression
infxrgelb	⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem infxrgelb Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrltso 13162	. . . . . 6 ⊢ < Or ℝ^*
2	1	a1i 11	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → < Or ℝ^*)
3		xrinfmss 13331	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → ∃𝑧 ∈ ℝ^* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀𝑦 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑥 ∈ 𝐴 𝑥 < 𝑦)))
4		id 22	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → 𝐴 ⊆ ℝ^*)
5	2, 3, 4	infglbb 9509	. . . 4 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (inf(𝐴, ℝ^, < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵))
6	5	notbid 318	. . 3 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (¬ inf(𝐴, ℝ^, < ) < 𝐵 ↔ ¬ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵))
7		ralnex 3063	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ↔ ¬ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵)
8	6, 7	bitr4di 289	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (¬ inf(𝐴, ℝ^, < ) < 𝐵 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵))
9		id 22	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ∈ ℝ^*)
10		infxrcl 13355	. . 3 ⊢ (𝐴 ⊆ ℝ^* → inf(𝐴, ℝ^, < ) ∈ ℝ^)
11		xrlenlt 11305	. . 3 ⊢ ((𝐵 ∈ ℝ^* ∧ inf(𝐴, ℝ^, < ) ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ¬ inf(𝐴, ℝ^, < ) < 𝐵))
12	9, 10, 11	syl2anr 597	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ¬ inf(𝐴, ℝ^*, < ) < 𝐵))
13		simplr 768	. . . 4 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ^)
14		simpl 482	. . . . 5 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐴 ⊆ ℝ^)
15	14	sselda 3963	. . . 4 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ^)
16	13, 15	xrlenltd 11306	. . 3 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵))
17	16	ralbidva 3162	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵))
18	8, 12, 17	3bitr4d 311	1 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 ⊆ wss 3931 class class class wbr 5124 Or wor 5565 infcinf 9458 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-po 5566 df-so 5567 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474

This theorem is referenced by: infxrre 13358 infxrss 13361 ixxlb 13389 limsuple 15499 limsupval2 15501 imasdsf1olem 24317 nmogelb 24660 metdsf 24793 metdsge 24794 ovolgelb 25438 ovolge0 25439 ovolsslem 25442 ovolicc2 25480 ismblfin 37690 infrpge 45345 infleinf2 45408 infxrgelbrnmpt 45448 inficc 45530 liminfgord 45750 liminflelimsuplem 45771 ovnhoilem2 46598

W3C validator