ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  infregelbex GIF version

Theorem infregelbex 9598
Description: Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
Hypotheses
Ref Expression
infregelbex.ex (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧𝐴 𝑧 < 𝑦)))
infregelbex.ss (𝜑𝐴 ⊆ ℝ)
infregelbex.b (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
infregelbex (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧𝐴 𝐵𝑧))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧

Proof of Theorem infregelbex
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 infregelbex.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
21ad2antrr 488 . . . . 5 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → 𝐵 ∈ ℝ)
3 lttri3 8037 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑏 = 𝑐 ↔ (¬ 𝑏 < 𝑐 ∧ ¬ 𝑐 < 𝑏)))
43adantl 277 . . . . . . 7 ((𝜑 ∧ (𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ)) → (𝑏 = 𝑐 ↔ (¬ 𝑏 < 𝑐 ∧ ¬ 𝑐 < 𝑏)))
5 infregelbex.ex . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧𝐴 𝑧 < 𝑦)))
64, 5infclti 7022 . . . . . 6 (𝜑 → inf(𝐴, ℝ, < ) ∈ ℝ)
76ad2antrr 488 . . . . 5 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → inf(𝐴, ℝ, < ) ∈ ℝ)
8 infregelbex.ss . . . . . . 7 (𝜑𝐴 ⊆ ℝ)
98sselda 3156 . . . . . 6 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
109adantlr 477 . . . . 5 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → 𝑎 ∈ ℝ)
11 simplr 528 . . . . 5 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → 𝐵 ≤ inf(𝐴, ℝ, < ))
126adantr 276 . . . . . . 7 ((𝜑𝑎𝐴) → inf(𝐴, ℝ, < ) ∈ ℝ)
134, 5inflbti 7023 . . . . . . . 8 (𝜑 → (𝑎𝐴 → ¬ 𝑎 < inf(𝐴, ℝ, < )))
1413imp 124 . . . . . . 7 ((𝜑𝑎𝐴) → ¬ 𝑎 < inf(𝐴, ℝ, < ))
1512, 9, 14nltled 8078 . . . . . 6 ((𝜑𝑎𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑎)
1615adantlr 477 . . . . 5 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑎)
172, 7, 10, 11, 16letrd 8081 . . . 4 (((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) ∧ 𝑎𝐴) → 𝐵𝑎)
1817ralrimiva 2550 . . 3 ((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) → ∀𝑎𝐴 𝐵𝑎)
19 breq2 4008 . . . 4 (𝑎 = 𝑧 → (𝐵𝑎𝐵𝑧))
2019cbvralv 2704 . . 3 (∀𝑎𝐴 𝐵𝑎 ↔ ∀𝑧𝐴 𝐵𝑧)
2118, 20sylib 122 . 2 ((𝜑𝐵 ≤ inf(𝐴, ℝ, < )) → ∀𝑧𝐴 𝐵𝑧)
221adantr 276 . . 3 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → 𝐵 ∈ ℝ)
236adantr 276 . . 3 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → inf(𝐴, ℝ, < ) ∈ ℝ)
24 simpl 109 . . . 4 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → 𝜑)
25 simpr 110 . . . . . . . 8 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → ∀𝑧𝐴 𝐵𝑧)
26 breq2 4008 . . . . . . . . 9 (𝑧 = 𝑑 → (𝐵𝑧𝐵𝑑))
2726cbvralv 2704 . . . . . . . 8 (∀𝑧𝐴 𝐵𝑧 ↔ ∀𝑑𝐴 𝐵𝑑)
2825, 27sylib 122 . . . . . . 7 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → ∀𝑑𝐴 𝐵𝑑)
291ad2antrr 488 . . . . . . . . 9 (((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) ∧ 𝑑𝐴) → 𝐵 ∈ ℝ)
308ad2antrr 488 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) ∧ 𝑑𝐴) → 𝐴 ⊆ ℝ)
31 simpr 110 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) ∧ 𝑑𝐴) → 𝑑𝐴)
3230, 31sseldd 3157 . . . . . . . . 9 (((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) ∧ 𝑑𝐴) → 𝑑 ∈ ℝ)
3329, 32lenltd 8075 . . . . . . . 8 (((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) ∧ 𝑑𝐴) → (𝐵𝑑 ↔ ¬ 𝑑 < 𝐵))
3433ralbidva 2473 . . . . . . 7 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → (∀𝑑𝐴 𝐵𝑑 ↔ ∀𝑑𝐴 ¬ 𝑑 < 𝐵))
3528, 34mpbid 147 . . . . . 6 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → ∀𝑑𝐴 ¬ 𝑑 < 𝐵)
36 breq1 4007 . . . . . . . 8 (𝑑 = 𝑧 → (𝑑 < 𝐵𝑧 < 𝐵))
3736notbid 667 . . . . . . 7 (𝑑 = 𝑧 → (¬ 𝑑 < 𝐵 ↔ ¬ 𝑧 < 𝐵))
3837cbvralv 2704 . . . . . 6 (∀𝑑𝐴 ¬ 𝑑 < 𝐵 ↔ ∀𝑧𝐴 ¬ 𝑧 < 𝐵)
3935, 38sylib 122 . . . . 5 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → ∀𝑧𝐴 ¬ 𝑧 < 𝐵)
4022, 39jca 306 . . . 4 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → (𝐵 ∈ ℝ ∧ ∀𝑧𝐴 ¬ 𝑧 < 𝐵))
414, 5infnlbti 7025 . . . 4 (𝜑 → ((𝐵 ∈ ℝ ∧ ∀𝑧𝐴 ¬ 𝑧 < 𝐵) → ¬ inf(𝐴, ℝ, < ) < 𝐵))
4224, 40, 41sylc 62 . . 3 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → ¬ inf(𝐴, ℝ, < ) < 𝐵)
4322, 23, 42nltled 8078 . 2 ((𝜑 ∧ ∀𝑧𝐴 𝐵𝑧) → 𝐵 ≤ inf(𝐴, ℝ, < ))
4421, 43impbida 596 1 (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧𝐴 𝐵𝑧))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wcel 2148  wral 2455  wrex 2456  wss 3130   class class class wbr 4004  infcinf 6982  cr 7810   < clt 7992  cle 7993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-cnex 7902  ax-resscn 7903  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-apti 7926
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-xp 4633  df-cnv 4635  df-iota 5179  df-riota 5831  df-sup 6983  df-inf 6984  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998
This theorem is referenced by:  nninfdclemp1  12451
  Copyright terms: Public domain W3C validator