Metamath Proof Explorer

Theorem nadd1rabtr

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

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

Proof

Step Hyp Ref Expression
1 nadd2rabtr 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( B +no x ) e. C } )
2 simpl2 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> B 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 
 |-  ( ( B e. On /\ x e. On ) -> ( B +no x ) = ( x +no B ) )
6 2 4 5 syl2anc 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( B +no x ) = ( x +no B ) )
7 6 eleq1d 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C <-> ( x +no B ) e. C ) )
8 7 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 } )
9 treq 
 |-  ( { x e. A | ( B +no x ) e. C } = { x e. A | ( x +no B ) e. C } -> ( Tr { x e. A | ( B +no x ) e. C } <-> Tr { x e. A | ( x +no B ) e. C } ) )
10 8 9 syl 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> ( Tr { x e. A | ( B +no x ) e. C } <-> Tr { x e. A | ( x +no B ) e. C } ) )
11 1 10 mpbid 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( x +no B ) e. C } )