Metamath Proof Explorer

Theorem nadd2rabex

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

Proof

Step Hyp Ref Expression
1 simp3 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → C ∈ On
2 0elon ⊢ ∅ ∈ On
3 ordelon ⊢ Ord ⁡ A ∧ x ∈ A → x ∈ On
4 3 3ad2antl1 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x ∈ On
5 naddcom ⊢ ∅ ∈ On ∧ x ∈ On → ∅ + x = x + ∅
6 2 4 5 sylancr ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → ∅ + x = x + ∅
7 naddrid ⊢ x ∈ On → x + ∅ = x
8 4 7 syl ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x + ∅ = x
9 6 8 eqtrd ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → ∅ + x = x
10 0ss ⊢ ∅ ⊆ B
11 simpl2 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B ∈ On
12 naddssim ⊢ ∅ ∈ On ∧ B ∈ On ∧ x ∈ On → ∅ ⊆ B → ∅ + x ⊆ B + x
13 2 11 4 12 mp3an2i ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → ∅ ⊆ B → ∅ + x ⊆ B + x
14 10 13 mpi ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → ∅ + x ⊆ B + x
15 9 14 eqsstrrd ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x ⊆ B + x
16 simpl3 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → C ∈ On
17 ontr2 ⊢ x ∈ On ∧ C ∈ On → x ⊆ B + x ∧ B + x ∈ C → x ∈ C
18 4 16 17 syl2anc ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x ⊆ B + x ∧ B + x ∈ C → x ∈ C
19 15 18 mpand ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B + x ∈ C → x ∈ C
20 19 3impia ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A ∧ B + x ∈ C → x ∈ C
21 20 rabssdv ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | B + x ∈ C ⊆ C
22 1 21 ssexd ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | B + x ∈ C ∈ V