Theorem nadd2rabord

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	nadd2rabord	|- ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	|- { x e. A | ( B +no x ) e. C } C_ A
2		ordsson	|- ( Ord A -> A C_ On )
3	2	3ad2ant1	|- ( ( Ord A /\ B e. On /\ C e. On ) -> A C_ On )
4	1 3	sstrid	|- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ On )
5		nadd2rabtr	|- ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( B +no x ) e. C } )
6		dford5	|- ( Ord { x e. A | ( B +no x ) e. C } <-> ( { x e. A | ( B +no x ) e. C } C_ On /\ Tr { x e. A | ( B +no x ) e. C } ) )
7	4 5 6	sylanbrc	|- ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } )