This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrletrid

Description: Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrletrid.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrletrid.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
xrletrid.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
xrletrid.4 ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
Assertion xrletrid ( 𝜑 → 𝐴 = 𝐵 )

Proof

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