Theorem nadd2rabex

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

Proof

Step	Hyp	Ref	Expression
1		simp3	$$⊢\left(\mathrm{Ord}A\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to C\in \mathrm{On}$$
2		0elon	$$⊢\varnothing \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 ( ( (/) e. On /\ x e. On ) -> ( (/) +no x ) = ( x +no (/) ) ) : No typesetting found for |- ( ( (/) e. On /\ x e. On ) -> ( (/) +no x ) = ( x +no (/) ) ) with typecode |-
6	2 4 5	sylancr	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = ( x +no (/) ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = ( x +no (/) ) ) with typecode |-
7		naddrid	Could not format ( x e. On -> ( x +no (/) ) = x ) : No typesetting found for |- ( x e. On -> ( x +no (/) ) = x ) with typecode |-
8	4 7	syl	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( x +no (/) ) = x ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( x +no (/) ) = x ) with typecode |-
9	6 8	eqtrd	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = x ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) = x ) with typecode |-
10		0ss	$$⊢\varnothing \subseteq B$$
11		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}$$
12		naddssim	Could not format ( ( (/) e. On /\ B e. On /\ x e. On ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) ) : No typesetting found for |- ( ( (/) e. On /\ B e. On /\ x e. On ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) ) with typecode |-
13	2 11 4 12	mp3an2i	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) C_ B -> ( (/) +no x ) C_ ( B +no x ) ) ) with typecode |-
14	10 13	mpi	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) C_ ( B +no x ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( (/) +no x ) C_ ( B +no x ) ) with typecode |-
15	9 14	eqsstrrd	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> x C_ ( B +no x ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> x C_ ( B +no x ) ) with typecode |-
16		simpl3	$$⊢\left(\left(\mathrm{Ord}A\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in A\right)\to C\in \mathrm{On}$$
17		ontr2	Could not format ( ( x e. On /\ C e. On ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) ) : No typesetting found for |- ( ( x e. On /\ C e. On ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) ) with typecode |-
18	4 16 17	syl2anc	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( x C_ ( B +no x ) /\ ( B +no x ) e. C ) -> x e. C ) ) with typecode |-
19	15 18	mpand	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C -> x e. C ) ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A ) -> ( ( B +no x ) e. C -> x e. C ) ) with typecode |-
20	19	3impia	Could not format ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A /\ ( B +no x ) e. C ) -> x e. C ) : No typesetting found for |- ( ( ( Ord A /\ B e. On /\ C e. On ) /\ x e. A /\ ( B +no x ) e. C ) -> x e. C ) with typecode |-
21	20	rabssdv	Could not format ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ C ) : No typesetting found for |- ( ( Ord A /\ B e. On /\ C e. On ) -> { x e. A | ( B +no x ) e. C } C_ C ) with typecode |-
22	1 21	ssexd	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 |-