omun

Description: The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025)

		Ref	Expression
	Assertion	omun	$⊢ (A \in ω \land B \in ω) \to A \cup B \in ω$

Step	Hyp	Ref	Expression
1		ssequn1	$⊢ A \subseteq B \leftrightarrow A \cup B = B$
2		eleq1a	$⊢ B \in ω \to (A \cup B = B \to A \cup B \in ω)$
3	2	adantl	$⊢ (A \in ω \land B \in ω) \to (A \cup B = B \to A \cup B \in ω)$
4	1 3	biimtrid	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \to A \cup B \in ω)$
5		ssequn2	$⊢ B \subseteq A \leftrightarrow A \cup B = A$
6		eleq1a	$⊢ A \in ω \to (A \cup B = A \to A \cup B \in ω)$
7	6	adantr	$⊢ (A \in ω \land B \in ω) \to (A \cup B = A \to A \cup B \in ω)$
8	5 7	biimtrid	$⊢ (A \in ω \land B \in ω) \to (B \subseteq A \to A \cup B \in ω)$
9		nnord	$⊢ A \in ω \to Ord A$
10		nnord	$⊢ B \in ω \to Ord B$
11		ordtri2or2	$⊢ (Ord A \land Ord B) \to (A \subseteq B \lor B \subseteq A)$
12	9 10 11	syl2an	$⊢ (A \in ω \land B \in ω) \to (A \subseteq B \lor B \subseteq A)$
13	4 8 12	mpjaod	$⊢ (A \in ω \land B \in ω) \to A \cup B \in ω$

Metamath Proof Explorer