Metamath Proof Explorer

Theorem nadd1rabex

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

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B ∈ On
2 ordelon ⊢ Ord ⁡ A ∧ x ∈ A → x ∈ On
3 2 3ad2antl1 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x ∈ On
4 naddcom ⊢ B ∈ On ∧ x ∈ On → B + x = x + B
5 1 3 4 syl2anc ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B + x = x + B
6 5 eleq1d ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B + x ∈ C ↔ x + B ∈ C
7 6 rabbidva ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | B + x ∈ C = x ∈ A | x + B ∈ C
8 nadd2rabex ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | B + x ∈ C ∈ V
9 7 8 eqeltrrd ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | x + B ∈ C ∈ V