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 Could not format assertion : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( B +no x ) e. C } ) with typecode |-

Proof

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