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

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
2 0elon ⊢ ∅ ∈ On
3 ordelon ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
4 3 3ad2antl1 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
5 naddcom ⊢ ( ( ∅ ∈ On ∧ 𝑥 ∈ On ) → ( ∅ +no 𝑥 ) = ( 𝑥 +no ∅ ) )
6 2 4 5 sylancr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ∅ +no 𝑥 ) = ( 𝑥 +no ∅ ) )
7 naddrid ⊢ ( 𝑥 ∈ On → ( 𝑥 +no ∅ ) = 𝑥 )
8 4 7 syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 +no ∅ ) = 𝑥 )
9 6 8 eqtrd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ∅ +no 𝑥 ) = 𝑥 )
10 0ss ⊢ ∅ ⊆ 𝐵
11 simpl2 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ On )
12 naddssim ⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ⊆ 𝐵 → ( ∅ +no 𝑥 ) ⊆ ( 𝐵 +no 𝑥 ) ) )
13 2 11 4 12 mp3an2i ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ∅ ⊆ 𝐵 → ( ∅ +no 𝑥 ) ⊆ ( 𝐵 +no 𝑥 ) ) )
14 10 13 mpi ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ∅ +no 𝑥 ) ⊆ ( 𝐵 +no 𝑥 ) )
15 9 14 eqsstrrd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐵 +no 𝑥 ) )
16 simpl3 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ On )
17 ontr2 ⊢ ( ( 𝑥 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝑥 ⊆ ( 𝐵 +no 𝑥 ) ∧ ( 𝐵 +no 𝑥 ) ∈ 𝐶 ) → 𝑥 ∈ 𝐶 ) )
18 4 16 17 syl2anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ⊆ ( 𝐵 +no 𝑥 ) ∧ ( 𝐵 +no 𝑥 ) ∈ 𝐶 ) → 𝑥 ∈ 𝐶 ) )
19 15 18 mpand ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 +no 𝑥 ) ∈ 𝐶 → 𝑥 ∈ 𝐶 ) )
20 19 3impia ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐵 +no 𝑥 ) ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
21 20 rabssdv ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ⊆ 𝐶 )
22 1 21 ssexd ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ∈ V )