Metamath Proof Explorer

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

Proof

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