Metamath Proof Explorer

Theorem nadd2rabon

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

Ref Expression
Assertion nadd2rabon 
|- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. On )

Proof

Step Hyp Ref Expression
1 nadd2rabord 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } )
2 nadd2rabex 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. _V )
3 elon2 
 |-  ( { x e. A | ( B +no x ) e. C } e. On <-> ( Ord { x e. A | ( B +no x ) e. C } /\ { x e. A | ( B +no x ) e. C } e. _V ) )
4 1 2 3 sylanbrc 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. On )