Metamath Proof Explorer

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 ⁡ A ∧ B ∈ On ∧ C ∈ On → Tr ⁡ x ∈ A | x + B ∈ C

Proof

Step Hyp Ref Expression
1 nadd2rabtr ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → Tr ⁡ x ∈ A | B + x ∈ C
2 simpl2 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B ∈ On
3 ordelon ⊢ Ord ⁡ A ∧ x ∈ A → x ∈ On
4 3 3ad2antl1 ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → x ∈ On
5 naddcom ⊢ B ∈ On ∧ x ∈ On → B + x = x + B
6 2 4 5 syl2anc ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B + x = x + B
7 6 eleq1d ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On ∧ x ∈ A → B + x ∈ C ↔ x + B ∈ C
8 7 rabbidva ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → x ∈ A | B + x ∈ C = x ∈ A | x + B ∈ C
9 treq ⊢ x ∈ A | B + x ∈ C = x ∈ A | x + B ∈ C → Tr ⁡ x ∈ A | B + x ∈ C ↔ Tr ⁡ x ∈ A | x + B ∈ C
10 8 9 syl ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → Tr ⁡ x ∈ A | B + x ∈ C ↔ Tr ⁡ x ∈ A | x + B ∈ C
11 1 10 mpbid ⊢ Ord ⁡ A ∧ B ∈ On ∧ C ∈ On → Tr ⁡ x ∈ A | x + B ∈ C