Theorem ordunmax

Description: The union of two ordinals is equal to their maximum. (Contributed by BTernaryTau, 7-Oct-2026)

	Ref	Expression
Assertion	ordunmax	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to A\cup B=if\left(A\subseteq B,B,A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtri2or2	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\vee B\subseteq A\right)$$
2	1	ord	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\neg A\subseteq B\to B\subseteq A\right)$$
3		ssequn2	$$⊢B\subseteq A\leftrightarrow A\cup B=A$$
4	2 3	imbitrdi	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\neg A\subseteq B\to A\cup B=A\right)$$
5		iffalse	$$⊢\neg A\subseteq B\to if\left(A\subseteq B,B,A\right)=A$$
6	4 5	jca2	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\neg A\subseteq B\to \left(A\cup B=A\wedge if\left(A\subseteq B,B,A\right)=A\right)\right)$$
7		eqtr3	$$⊢\left(A\cup B=A\wedge if\left(A\subseteq B,B,A\right)=A\right)\to A\cup B=if\left(A\subseteq B,B,A\right)$$
8	6 7	syl6	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\neg A\subseteq B\to A\cup B=if\left(A\subseteq B,B,A\right)\right)$$
9		ssequn1	$$⊢A\subseteq B\leftrightarrow A\cup B=B$$
10	9	biimpi	$$⊢A\subseteq B\to A\cup B=B$$
11		iftrue	$$⊢A\subseteq B\to if\left(A\subseteq B,B,A\right)=B$$
12	10 11	eqtr4d	$$⊢A\subseteq B\to A\cup B=if\left(A\subseteq B,B,A\right)$$
13	8 12	pm2.61d2	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to A\cup B=if\left(A\subseteq B,B,A\right)$$