Metamath Proof Explorer

Theorem nadd2rabtr

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

Proof

Step Hyp Ref Expression
1 simpll1 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> Ord A )
2 simplr 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> y e. A )
3 ordelss 
 |-  ( ( Ord A /\ y e. A ) -> y C_ A )
4 1 2 3 syl2anc 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> y C_ A )
5 simpll3 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> C e. On )
6 5 adantr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> C e. On )
7 simpr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> x e. y )
8 1 adantr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> Ord A )
9 simpllr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> y e. A )
10 ordelon 
 |-  ( ( Ord A /\ y e. A ) -> y e. On )
11 8 9 10 syl2anc 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> y e. On )
12 onelon 
 |-  ( ( y e. On /\ x e. y ) -> x e. On )
13 11 7 12 syl2anc 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> x e. On )
14 simpll2 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> B e. On )
15 14 adantr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> B e. On )
16 naddel2 
 |-  ( ( x e. On /\ y e. On /\ B e. On ) -> ( x e. y <-> ( B +no x ) e. ( B +no y ) ) )
17 13 11 15 16 syl3anc 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> ( x e. y <-> ( B +no x ) e. ( B +no y ) ) )
18 7 17 mpbid 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> ( B +no x ) e. ( B +no y ) )
19 simplr 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> ( B +no y ) e. C )
20 18 19 jca 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> ( ( B +no x ) e. ( B +no y ) /\ ( B +no y ) e. C ) )
21 ontr1 
 |-  ( C e. On -> ( ( ( B +no x ) e. ( B +no y ) /\ ( B +no y ) e. C ) -> ( B +no x ) e. C ) )
22 6 20 21 sylc 
 |-  ( ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) /\ x e. y ) -> ( B +no x ) e. C )
23 4 22 ssrabdv 
 |-  ( ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) /\ ( B +no y ) e. C ) -> y C_ { x e. A | ( B +no x ) e. C } )
24 23 ex 
 |-  ( ( ( Ord A /\ B e. On /\ C e. On ) /\ y e. A ) -> ( ( B +no y ) e. C -> y C_ { x e. A | ( B +no x ) e. C } ) )
25 24 ralrimiva 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> A. y e. A ( ( B +no y ) e. C -> y C_ { x e. A | ( B +no x ) e. C } ) )
26 oveq2 
 |-  ( x = y -> ( B +no x ) = ( B +no y ) )
27 26 eleq1d 
 |-  ( x = y -> ( ( B +no x ) e. C <-> ( B +no y ) e. C ) )
28 27 ralrab 
 |-  ( A. y e. { x e. A | ( B +no x ) e. C } y C_ { x e. A | ( B +no x ) e. C } <-> A. y e. A ( ( B +no y ) e. C -> y C_ { x e. A | ( B +no x ) e. C } ) )
29 25 28 sylibr 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> A. y e. { x e. A | ( B +no x ) e. C } y C_ { x e. A | ( B +no x ) e. C } )
30 dftr3 
 |-  ( Tr { x e. A | ( B +no x ) e. C } <-> A. y e. { x e. A | ( B +no x ) e. C } y C_ { x e. A | ( B +no x ) e. C } )
31 29 30 sylibr 
 |-  ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( B +no x ) e. C } )