Theorem xrletrid 13154

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 13153	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
6	3, 4, 5	syl2anc 593	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
7	1, 2, 6	mpbir2and 723	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141   class class class wbr 5099  ℝ^*cxr 11212   ≤ cle 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-pre-lttri 11144  ax-pre-lttrn 11145

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-po 5553  df-so 5554  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219

This theorem is referenced by:  supxrre  13327  infxrre  13337  ixxub  13367  ixxlb  13368  pcadd2  16909  psmetsym  24350  xmetsym  24387  imasdsf1olem  24413  ovolunnul  25542  ovolicc  25565  voliunlem3  25594  uniioovol  25621  uniiccvol  25622  ismbfd  25681  mbflimsup  25708  itg2itg1  25778  itg2seq  25784  itg2eqa  25787  itg2split  25791  itg2mono  25795  deg1add  26143  deg1mul2  26154  deg1tm  26159  xrgepnfd  45871  supxrge  45878  infxrpnf  45984  eliccnelico  46069  liminfgelimsup  46320  liminfgelimsupuz  46326  liminflimsupclim  46345  xlimliminflimsup  46400  ismbl4  46531  rrxsnicc  46838  sge0fsum  46925  sge0split  46947  sge0iunmptlemre  46953  sge0isum  46965  sge0xaddlem2  46972  sge0reuz  46985  meale0eq0  47016  carageniuncl  47061  caratheodorylem2  47065  caragenel2d  47070  omess0  47072  ovn0lem  47103  hoidmv1lelem2  47130  hoidmv1lelem3  47131  hoidmvlelem4  47136  ovnhoi  47141  ovolval2lem  47181  ovolval5lem3  47192