Theorem xrletrid 12962

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105   class class class wbr 5087  ℝ^*cxr 11081   ≤ cle 11083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-pre-lttri 11018  ax-pre-lttrn 11019

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-po 5521  df-so 5522  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088

This theorem is referenced by:  supxrre  13134  infxrre  13143  ixxub  13173  ixxlb  13174  pcadd2  16661  psmetsym  23535  xmetsym  23572  imasdsf1olem  23598  ovolunnul  24736  ovolicc  24759  voliunlem3  24788  uniioovol  24815  uniiccvol  24816  ismbfd  24875  mbflimsup  24902  itg2itg1  24973  itg2seq  24979  itg2eqa  24982  itg2split  24986  itg2mono  24990  deg1add  25340  deg1mul2  25351  deg1tm  25355  xrgepnfd  43106  supxrge  43113  infxrpnf  43222  eliccnelico  43304  liminfgelimsup  43560  liminfgelimsupuz  43566  liminflimsupclim  43585  xlimliminflimsup  43640  ismbl4  43771  rrxsnicc  44078  sge0fsum  44163  sge0split  44185  sge0iunmptlemre  44191  sge0isum  44203  sge0xaddlem2  44210  sge0reuz  44223  meale0eq0  44254  carageniuncl  44299  caratheodorylem2  44303  caragenel2d  44308  omess0  44310  ovn0lem  44341  hoidmv1lelem2  44368  hoidmv1lelem3  44369  hoidmvlelem4  44374  ovnhoi  44379  ovolval2lem  44419  ovolval5lem3  44430