nadd1rabord

Description: The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024)

		Ref	Expression
	Assertion	nadd1rabord	$⊢ (Ord A \land B \in On \land C \in On) \to Ord \{x \in A \| x + B \in C\}$

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{x \in A \| x + B \in C\} \subseteq A$
2		ordsson	$⊢ Ord A \to A \subseteq On$
3	2	3ad2ant1	$⊢ (Ord A \land B \in On \land C \in On) \to A \subseteq On$
4	1 3	sstrid	$⊢ (Ord A \land B \in On \land C \in On) \to \{x \in A \| x + B \in C\} \subseteq On$
5		nadd1rabtr	$⊢ (Ord A \land B \in On \land C \in On) \to Tr \{x \in A \| x + B \in C\}$
6		dford5	$⊢ Ord \{x \in A \| x + B \in C\} \leftrightarrow (\{x \in A \| x + B \in C\} \subseteq On \land Tr \{x \in A \| x + B \in C\})$
7	4 5 6	sylanbrc	$⊢ (Ord A \land B \in On \land C \in On) \to Ord \{x \in A \| x + B \in C\}$

Metamath Proof Explorer