Theorem ordun

Description: The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of TakeutiZaring p. 40. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	ordun	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \mathrm{Ord}\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A\cup B=A\cup B$$
2		ordequn	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\cup B=A\cup B\to \left(A\cup B=A\vee A\cup B=B\right)\right)$$
3	1 2	mpi	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\cup B=A\vee A\cup B=B\right)$$
4		ordeq	$$⊢A\cup B=A\to \left(\mathrm{Ord}\left(A\cup B\right)\leftrightarrow \mathrm{Ord}A\right)$$
5	4	biimprcd	$$⊢\mathrm{Ord}A\to \left(A\cup B=A\to \mathrm{Ord}\left(A\cup B\right)\right)$$
6		ordeq	$$⊢A\cup B=B\to \left(\mathrm{Ord}\left(A\cup B\right)\leftrightarrow \mathrm{Ord}B\right)$$
7	6	biimprcd	$$⊢\mathrm{Ord}B\to \left(A\cup B=B\to \mathrm{Ord}\left(A\cup B\right)\right)$$
8	5 7	jaao	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(\left(A\cup B=A\vee A\cup B=B\right)\to \mathrm{Ord}\left(A\cup B\right)\right)$$
9	3 8	mpd	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \mathrm{Ord}\left(A\cup B\right)$$