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 13339

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 13143	. . . . . 6 ⊢ < Or ℝ^*
2	1	a1i 11	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → < Or ℝ^*)
3		xrinfmss 13313	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → ∃𝑧 ∈ ℝ^* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀𝑦 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑥 ∈ 𝐴 𝑥 < 𝑦)))
4		id 22	. . . . 5 ⊢ (𝐴 ⊆ ℝ^* → 𝐴 ⊆ ℝ^*)
5	2, 3, 4	infglbb 9438	. . . 4 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (inf(𝐴, ℝ^, < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵))
6	5	notbid 320	. . 3 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (¬ inf(𝐴, ℝ^, < ) < 𝐵 ↔ ¬ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵))
7		ralnex 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ↔ ¬ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵)
8	6, 7	bitr4di 291	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (¬ inf(𝐴, ℝ^, < ) < 𝐵 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵))
9		id 22	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ∈ ℝ^*)
10		infxrcl 13337	. . 3 ⊢ (𝐴 ⊆ ℝ^* → inf(𝐴, ℝ^, < ) ∈ ℝ^)
11		xrlenlt 11247	. . 3 ⊢ ((𝐵 ∈ ℝ^* ∧ inf(𝐴, ℝ^, < ) ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ¬ inf(𝐴, ℝ^, < ) < 𝐵))
12	9, 10, 11	syl2anr 606	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ¬ inf(𝐴, ℝ^*, < ) < 𝐵))
13		simplr 778	. . . 4 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ^)
14		simpl 486	. . . . 5 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → 𝐴 ⊆ ℝ^)
15	14	sselda 3936	. . . 4 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ^)
16	13, 15	xrlenltd 11248	. . 3 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵))
17	16	ralbidva 3183	. 2 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵))
18	8, 12, 17	3bitr4d 313	1 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ≤ inf(𝐴, ℝ^, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∈ wcel 2142 ∀wral 3076 ∃wrex 3086 ⊆ wss 3904 class class class wbr 5100 Or wor 5554 infcinf 9387 ℝ^*cxr 11215 < clt 11216 ≤ cle 11217

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-po 5555 df-so 5556 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-er 8678 df-en 8928 df-dom 8929 df-sdom 8930 df-sup 9388 df-inf 9389 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417

This theorem is referenced by: infxrre 13340 infxrss 13343 ixxlb 13371 limsuple 15505 limsupval2 15507 imasdsf1olem 24433 nmogelb 24776 metdsf 24909 metdsge 24910 ovolgelb 25542 ovolge0 25543 ovolsslem 25546 ovolicc2 25584 ismblfin 38160 infrpge 45927 infleinf2 45988 infxrgelbrnmpt 46028 inficc 46110 liminfgord 46328 liminflelimsuplem 46349 ovnhoilem2 47176

W3C validator