Theorem nadd2rabord

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

	Ref	Expression
Assertion	nadd2rabord	Could not format assertion : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssrab2	Could not format { x e. A | ( B +no x ) e. C } C_ A : No typesetting found for |- { x e. A | ( B +no x ) e. C } C_ A with typecode |-
2		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
3	2	3ad2ant1	$$⊢\left(\mathrm{Ord}A\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to A\subseteq \mathrm{On}$$
4	1 3	sstrid	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ On ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ On ) with typecode |-
5		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 |-
6		dford5	Could not format ( Ord { x e. A | ( B +no x ) e. C } <-> ( { x e. A | ( B +no x ) e. C } C_ On /\ Tr { x e. A | ( B +no x ) e. C } ) ) : No typesetting found for |- ( Ord { x e. A | ( B +no x ) e. C } <-> ( { x e. A | ( B +no x ) e. C } C_ On /\ Tr { x e. A | ( B +no x ) e. C } ) ) with typecode |-
7	4 5 6	sylanbrc	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> Ord { x e. A | ( B +no x ) e. C } ) with typecode |-