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

Theorem xrlenlt 10357
Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
xrlenlt ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem xrlenlt
StepHypRef Expression
1 df-br 4810 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 5314 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 10334 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2836 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3742 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 266 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 531 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 17 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8syl5bb 274 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 opelcnvg 5470 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
11 df-br 4810 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
1210, 11syl6rbbr 281 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ < ))
1312notbid 309 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
149, 13bitr4d 273 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wcel 2155  cdif 3729  cop 4340   class class class wbr 4809   × cxp 5275  ccnv 5276  *cxr 10327   < clt 10328  cle 10329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810  df-opab 4872  df-xp 5283  df-cnv 5285  df-le 10334
This theorem is referenced by:  xrlenltd  10358  xrltnle  10359  xrnltled  10360  lenlt  10370  pnfge  12164  mnfle  12169  xrleloe  12177  xrltlen  12179  xrletri3  12187  xgepnf  12198  xlemnf  12200  xralrple  12238  xleneg  12251  supxr2  12346  supxrbnd1  12353  supxrbnd2  12354  supxrub  12356  supxrleub  12358  supxrbnd  12360  infxrgelb  12367  ixxub  12398  ioon0  12403  iccid  12422  icc0  12425  icoun  12501  icodisj  12502  ioounsn  12503  ioounsnOLD  12504  snunico  12506  ioodisj  12509  ioojoin  12510  supicclub2  12530  hashgt0elex  13390  hashgt12el  13411  hashgt12el2  13412  0ringnnzr  19543  lecldbas  21303  xmetgt0  22442  bldisj  22482  icopnfcld  22850  icombl  23622  ioombl  23623  ioorcl2  23630  vitalilem4  23669  itg2gt0  23818  ply1divmo  24186  ig1peu  24222  radcnvle  24465  psercnlem1  24470  nmlnogt0  28043  xrlelttric  29901  xrsupssd  29908  xrge0infss  29909  joiniooico  29920  xeqlelt  29922  iocinif  29927  esumsnf  30508  esum2d  30537  oms0  30741  omssubadd  30744  relowlpssretop  33577  mblfinlem3  33804  mblfinlem4  33805  ismblfin  33806  asindmre  33850  iocmbl  38406  supxrgere  40119  iccdifprioo  40313  iccpartnel  42040
  Copyright terms: Public domain W3C validator