Metamath Proof Explorer

Theorem naddss2

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

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

Proof

Step Hyp Ref Expression
1 naddss1 ⊢ 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 sseq12d ⊢ 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