Theorem nadd1rabex

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

Proof

Step	Hyp	Ref	Expression
1		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}$$
2		ordelon	$$⊢\left(\mathrm{Ord}A\wedge x\in A\right)\to x\in \mathrm{On}$$
3	2	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}$$
4		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 |-
5	1 3 4	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 |-
6	5	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 |-
7	6	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 |-
8		nadd2rabex	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. _V ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } e. _V ) with typecode |-
9	7 8	eqeltrrd	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( x +no B ) e. C } e. _V ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( x +no B ) e. C } e. _V ) with typecode |-