Metamath Proof Explorer

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 ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | x + B ∈ C ∈ On

Proof

Step Hyp Ref Expression
1 nadd1rabord ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → Ord ⁡ x ∈ A | x + B ∈ C
2 nadd1rabex ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | x + B ∈ C ∈ V
3 elon2 ⊢ x ∈ A | x + B ∈ C ∈ On ↔ Ord ⁡ x ∈ A | x + B ∈ C ∧ x ∈ A | x + B ∈ C ∈ V
4 1 2 3 sylanbrc ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | x + B ∈ C ∈ On