Theorem xrletrid 13138

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

Step	Hyp	Ref	Expression
1		xrletrid.3	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		xrletrid.4	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
3		xrletrid.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
4		xrletrid.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		xrletri3 13137	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
6	3, 4, 5	syl2anc 582	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
7	1, 2, 6	mpbir2and 709	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   class class class wbr 5147  ℝ^*cxr 11251   ≤ cle 11253

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-pre-lttri 11186  ax-pre-lttrn 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258

This theorem is referenced by:  supxrre  13310  infxrre  13319  ixxub  13349  ixxlb  13350  pcadd2  16827  psmetsym  24036  xmetsym  24073  imasdsf1olem  24099  ovolunnul  25249  ovolicc  25272  voliunlem3  25301  uniioovol  25328  uniiccvol  25329  ismbfd  25388  mbflimsup  25415  itg2itg1  25486  itg2seq  25492  itg2eqa  25495  itg2split  25499  itg2mono  25503  deg1add  25856  deg1mul2  25867  deg1tm  25871  xrgepnfd  44339  supxrge  44346  infxrpnf  44454  eliccnelico  44540  liminfgelimsup  44796  liminfgelimsupuz  44802  liminflimsupclim  44821  xlimliminflimsup  44876  ismbl4  45007  rrxsnicc  45314  sge0fsum  45401  sge0split  45423  sge0iunmptlemre  45429  sge0isum  45441  sge0xaddlem2  45448  sge0reuz  45461  meale0eq0  45492  carageniuncl  45537  caratheodorylem2  45541  caragenel2d  45546  omess0  45548  ovn0lem  45579  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmvlelem4  45612  ovnhoi  45617  ovolval2lem  45657  ovolval5lem3  45668