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

Proof

Step	Hyp	Ref	Expression
1		simpl2	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ On )
2		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
3	2	3ad2antl1	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
4		naddcom	⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 +no 𝑥 ) = ( 𝑥 +no 𝐵 ) )
5	1 3 4	syl2anc	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 +no 𝑥 ) = ( 𝑥 +no 𝐵 ) )
6	5	eleq1d	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 +no 𝑥 ) ∈ 𝐶 ↔ ( 𝑥 +no 𝐵 ) ∈ 𝐶 ) )
7	6	rabbidva	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } )
8		nadd2rabex	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ∈ V )
9	7 8	eqeltrrd	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ∈ V )