Theorem 2resupmax

Description: The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021)

	Ref	Expression
Assertion	2resupmax	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to sup\left(\left\{A,B\right\},ℝ,<\right)=if\left(A\le B,B,A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltso	$$⊢<\mathrm{Or}ℝ$$
2		suppr	$$⊢\left(<\mathrm{Or}ℝ\wedge A\in ℝ\wedge B\in ℝ\right)\to sup\left(\left\{A,B\right\},ℝ,<\right)=if\left(B<A,A,B\right)$$
3	1 2	mp3an1	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to sup\left(\left\{A,B\right\},ℝ,<\right)=if\left(B<A,A,B\right)$$
4		ifnot	$$⊢if\left(\neg B<A,B,A\right)=if\left(B<A,A,B\right)$$
5		lenlt	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
6	5	bicomd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\neg B<A\leftrightarrow A\le B\right)$$
7	6	ifbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to if\left(\neg B<A,B,A\right)=if\left(A\le B,B,A\right)$$
8	4 7	eqtr3id	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to if\left(B<A,A,B\right)=if\left(A\le B,B,A\right)$$
9	3 8	eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to sup\left(\left\{A,B\right\},ℝ,<\right)=if\left(A\le B,B,A\right)$$