Theorem xrletrid

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

	Ref	Expression
Hypotheses	xrletrid.1	|- ( ph -> A e. RR* )
	xrletrid.2	|- ( ph -> B e. RR* )
	xrletrid.3	|- ( ph -> A <_ B )
	xrletrid.4	|- ( ph -> B <_ A )
Assertion	xrletrid	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		xrletrid.1	|- ( ph -> A e. RR* )
2		xrletrid.2	|- ( ph -> B e. RR* )
3		xrletrid.3	|- ( ph -> A <_ B )
4		xrletrid.4	|- ( ph -> B <_ A )
5		xrletri3	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
6	1 2 5	syl2anc	|- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
7	3 4 6	mpbir2and	|- ( ph -> A = B )