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

Proof

Step	Hyp	Ref	Expression
1		nadd2rabtr	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 |-
2		simpl2	$$⊢\left(\left(\mathrm{Ord}A\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in A\right)\to B\in \mathrm{On}$$
3		ordelon	$$⊢\left(\mathrm{Ord}A\wedge x\in A\right)\to x\in \mathrm{On}$$
4	3	3ad2antl1	$$⊢\left(\left(\mathrm{Ord}A\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in A\right)\to x\in \mathrm{On}$$
5		naddcom	Could not format ( ( B e. On /\ x e. On ) -> ( B +no x ) = ( x +no B ) ) : No typesetting found for |- ( ( B e. On /\ x e. On ) -> ( B +no x ) = ( x +no B ) ) with typecode |-
6	2 4 5	syl2anc	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( B +no x ) = ( x +no B ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( B +no x ) = ( x +no B ) ) with typecode |-
7	6	eleq1d	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C <-> ( x +no B ) e. C ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C <-> ( x +no B ) e. C ) ) with typecode |-
8	7	rabbidva	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } = { x e. A | ( x +no B ) e. C } ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } = { x e. A | ( x +no B ) e. C } ) with typecode |-
9		treq	Could not format ( { 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 } ) ) : No typesetting found for |- ( { 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 } ) ) with typecode |-
10	8 9	syl	Could not format ( ( 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 } ) ) : No typesetting found for |- ( ( 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 } ) ) with typecode |-
11	1 10	mpbid	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( x +no B ) e. C } ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> Tr { x e. A | ( x +no B ) e. C } ) with typecode |-