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	$⊢ (Ord A \land Ord B) \to Ord (A \cup B)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ A \cup B = A \cup B$
2		ordequn	$⊢ (Ord A \land Ord B) \to (A \cup B = A \cup B \to (A \cup B = A \lor A \cup B = B))$
3	1 2	mpi	$⊢ (Ord A \land Ord B) \to (A \cup B = A \lor A \cup B = B)$
4		ordeq	$⊢ A \cup B = A \to (Ord (A \cup B) \leftrightarrow Ord A)$
5	4	biimprcd	$⊢ Ord A \to (A \cup B = A \to Ord (A \cup B))$
6		ordeq	$⊢ A \cup B = B \to (Ord (A \cup B) \leftrightarrow Ord B)$
7	6	biimprcd	$⊢ Ord B \to (A \cup B = B \to Ord (A \cup B))$
8	5 7	jaao	$⊢ (Ord A \land Ord B) \to ((A \cup B = A \lor A \cup B = B) \to Ord (A \cup B))$
9	3 8	mpd	$⊢ (Ord A \land Ord B) \to Ord (A \cup B)$

Metamath Proof Explorer