Theorem nadd1rabon

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

	Ref	Expression
Assertion	nadd1rabon	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ On )

Proof

Step	Hyp	Ref	Expression
1		nadd1rabord	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Ord { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } )
2		nadd1rabex	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ V )
3		elon2	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ On ↔ ( Ord { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∧ { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ V ) )
4	1 2 3	sylanbrc	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ On )