Theorem nadd1rabex

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl2	|- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> B e. On )
2		ordelon	|- ( ( Ord A /\ x e. A ) -> x e. On )
3	2	3ad2antl1	|- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> x e. On )
4		naddcom	|- ( ( B e. On /\ x e. On ) -> ( B +no x ) = ( x +no B ) )
5	1 3 4	syl2anc	|- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( B +no x ) = ( x +no B ) )
6	5	eleq1d	|- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C <-> ( x +no B ) e. C ) )
7	6	rabbidva	|- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } = { x e. A | ( x +no B ) e. C } )
8		nadd2rabex	|- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. _V )
9	7 8	eqeltrrd	|- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( x +no B ) e. C } e. _V )