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

Theorem xrlenlt 11326
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 5144 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 5722 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 11301 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2833 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3961 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 275 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 535 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 17 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8bitrid 283 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 df-br 5144 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11 opelcnvg 5891 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
1210, 11bitr4id 290 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ < ))
1312notbid 318 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
149, 13bitr4d 282 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wcel 2108  cdif 3948  cop 4632   class class class wbr 5143   × cxp 5683  ccnv 5684  *cxr 11294   < clt 11295  cle 11296
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-le 11301
This theorem is referenced by:  xrlenltd  11327  xrltnle  11328  lenlt  11339  pnfge  13172  mnfle  13177  xrleloe  13186  xrltlen  13188  xrletri3  13196  xgepnf  13207  xlemnf  13209  xralrple  13247  xleneg  13260  supxr2  13356  supxrbnd1  13363  supxrbnd2  13364  supxrleub  13368  supxrbnd  13370  infxrgelb  13377  ioon0  13413  iccid  13432  icc0  13435  icoun  13515  ioounsn  13517  snunico  13519  ioodisj  13522  ioojoin  13523  hashgt0elex  14440  hashgt12el  14461  hashgt12el2  14462  0ringnnzr  20525  lecldbas  23227  xmetgt0  24368  icopnfcld  24788  ioombl  25600  vitalilem4  25646  itg2gt0  25795  nmlnogt0  30816  xrlelttric  32756  xrsupssd  32763  xrge0infss  32764  joiniooico  32776  xeqlelt  32778  iocinif  32783  esumsnf  34065  esum2d  34094  oms0  34299  omssubadd  34302  cusgracyclt3v  35161  relowlpssretop  37365  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  asindmre  37710  dvrelog2b  42067  iocmbl  43225  supxrgere  45344  iccdifprioo  45529  iccpartnel  47425  iccdisj2  48795
  Copyright terms: Public domain W3C validator