Metamath Proof Explorer

Theorem naddel2

Description: Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024)

Ref Expression
Assertion naddel2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ C + A ∈ C + B

Proof

Step Hyp Ref Expression
1 naddel1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ A + C ∈ B + C
2 naddcom ⊢ A ∈ On ∧ C ∈ On → A + C = C + A
3 2 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + C = C + A
4 naddcom ⊢ B ∈ On ∧ C ∈ On → B + C = C + B
5 4 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C = C + B
6 3 5 eleq12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + C ∈ B + C ↔ C + A ∈ C + B
7 1 6 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ C + A ∈ C + B