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

Theorem xrlenlt 11280
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 5142 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 5706 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 11255 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2819 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3953 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 275 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 535 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 17 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8bitrid 283 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 df-br 5142 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11 opelcnvg 5873 . . . 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 205  wa 395  wcel 2098  cdif 3940  cop 4629   class class class wbr 5141   × cxp 5667  ccnv 5668  *cxr 11248   < clt 11249  cle 11250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5142  df-opab 5204  df-xp 5675  df-cnv 5677  df-le 11255
This theorem is referenced by:  xrlenltd  11281  xrltnle  11282  lenlt  11293  pnfge  13113  mnfle  13117  xrleloe  13126  xrltlen  13128  xrletri3  13136  xgepnf  13147  xlemnf  13149  xralrple  13187  xleneg  13200  supxr2  13296  supxrbnd1  13303  supxrbnd2  13304  supxrleub  13308  supxrbnd  13310  infxrgelb  13317  ioon0  13353  iccid  13372  icc0  13375  icoun  13455  ioounsn  13457  snunico  13459  ioodisj  13462  ioojoin  13463  hashgt0elex  14363  hashgt12el  14384  hashgt12el2  14385  0ringnnzr  20422  lecldbas  23073  xmetgt0  24214  icopnfcld  24634  ioombl  25444  vitalilem4  25490  itg2gt0  25640  nmlnogt0  30554  xrlelttric  32469  xrsupssd  32476  xrge0infss  32477  joiniooico  32489  xeqlelt  32491  iocinif  32496  esumsnf  33591  esum2d  33620  oms0  33825  omssubadd  33828  cusgracyclt3v  34674  relowlpssretop  36751  mblfinlem3  37039  mblfinlem4  37040  ismblfin  37041  asindmre  37083  dvrelog2b  41446  iocmbl  42520  supxrgere  44597  iccdifprioo  44783  iccpartnel  46660  iccdisj2  47786
  Copyright terms: Public domain W3C validator