Theorem nadd1rabtr

Description: The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024)

	Ref	Expression
Assertion	nadd1rabtr	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Tr { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		nadd2rabtr	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )
2		simpl2	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ On )
3		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
4	3	3ad2antl1	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
5		naddcom	⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 +no 𝑥 ) = ( 𝑥 +no 𝐵 ) )
6	2 4 5	syl2anc	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 +no 𝑥 ) = ( 𝑥 +no 𝐵 ) )
7	6	eleq1d	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 +no 𝑥 ) ∈ 𝐶 ↔ ( 𝑥 +no 𝐵 ) ∈ 𝐶 ) )
8	7	rabbidva	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } )
9		treq	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } → ( Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ↔ Tr { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ) )
10	8 9	syl	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ↔ Tr { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } ) )
11	1 10	mpbid	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Tr { 𝑥 ∈ 𝐴 ∣ ( 𝑥 +no 𝐵 ) ∈ 𝐶 } )