Metamath Proof Explorer

Theorem nadd2rabex

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

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> C e. On )
2 0elon 
 |-  (/) e. On
3 ordelon 
 |-  ( ( Ord A /\ x e. A ) -> x e. On )
4 3 3ad2antl1 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> x e. On )
5 naddcom 
 |-  ( ( (/) e. On /\ x e. On ) -> ( (/) +no x ) = ( x +no (/) ) )
6 2 4 5 sylancr 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = ( x +no (/) ) )
7 naddrid 
 |-  ( x e. On -> ( x +no (/) ) = x )
8 4 7 syl 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( x +no (/) ) = x )
9 6 8 eqtrd 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = x )
10 0ss 
 |-  (/) C_ B
11 simpl2 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> B e. On )
12 naddssim 
 |-  ( ( (/) e. On /\ B e. On /\ x e. On ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) )
13 2 11 4 12 mp3an2i 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) )
14 10 13 mpi 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) C_ ( B +no x ) )
15 9 14 eqsstrrd 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> x C_ ( B +no x ) )
16 simpl3 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> C e. On )
17 ontr2 
 |-  ( ( x e. On /\ C e. On ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) )
18 4 16 17 syl2anc 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) )
19 15 18 mpand 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C -> x e. C ) )
20 19 3impia 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A /\ ( B +no x ) e. C ) -> x e. C )
21 20 rabssdv 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ C )
22 1 21 ssexd 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. _V )