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

Theorem xrletrid 12545
Description: Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
xrletrid.1 (𝜑𝐴 ∈ ℝ*)
xrletrid.2 (𝜑𝐵 ∈ ℝ*)
xrletrid.3 (𝜑𝐴𝐵)
xrletrid.4 (𝜑𝐵𝐴)
Assertion
Ref Expression
xrletrid (𝜑𝐴 = 𝐵)

Proof of Theorem xrletrid
StepHypRef Expression
1 xrletrid.3 . 2 (𝜑𝐴𝐵)
2 xrletrid.4 . 2 (𝜑𝐵𝐴)
3 xrletrid.1 . . 3 (𝜑𝐴 ∈ ℝ*)
4 xrletrid.2 . . 3 (𝜑𝐵 ∈ ℝ*)
5 xrletri3 12544 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
63, 4, 5syl2anc 587 . 2 (𝜑 → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
71, 2, 6mpbir2and 712 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115   class class class wbr 5052  *cxr 10672  cle 10674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-resscn 10592  ax-pre-lttri 10609  ax-pre-lttrn 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-po 5461  df-so 5462  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679
This theorem is referenced by:  supxrre  12717  infxrre  12726  ixxub  12756  ixxlb  12757  pcadd2  16224  psmetsym  22920  xmetsym  22957  imasdsf1olem  22983  ovolunnul  24107  ovolicc  24130  voliunlem3  24159  uniioovol  24186  uniiccvol  24187  ismbfd  24246  mbflimsup  24273  itg2itg1  24343  itg2seq  24349  itg2eqa  24352  itg2split  24356  itg2mono  24360  deg1add  24707  deg1mul2  24718  deg1tm  24722  xrgepnfd  41889  supxrge  41896  infxrpnf  42010  eliccnelico  42092  liminfgelimsup  42350  liminfgelimsupuz  42356  liminflimsupclim  42375  xlimliminflimsup  42430  ismbl4  42561  rrxsnicc  42868  sge0fsum  42952  sge0split  42974  sge0iunmptlemre  42980  sge0isum  42992  sge0xaddlem2  42999  sge0reuz  43012  meale0eq0  43043  carageniuncl  43088  caratheodorylem2  43092  caragenel2d  43097  omess0  43099  ovn0lem  43130  hoidmv1lelem2  43157  hoidmv1lelem3  43158  hoidmvlelem4  43163  ovnhoi  43168  ovolval2lem  43208  ovolval5lem3  43219
  Copyright terms: Public domain W3C validator