Theorem nadd2rabon

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	nadd2rabon	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ∈ On )

Proof

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