Metamath Proof Explorer

Theorem naddss1

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

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

Proof

Step Hyp Ref Expression
1 naddel1 ⊢ B ∈ On ∧ A ∈ On ∧ C ∈ On → B ∈ A ↔ B + C ∈ A + C
2 1 3com12 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ∈ A ↔ B + C ∈ A + C
3 2 notbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ B ∈ A ↔ ¬ B + C ∈ A + C
4 ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A
5 4 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ ¬ B ∈ A
6 naddcl ⊢ A ∈ On ∧ C ∈ On → A + C ∈ On
7 6 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + C ∈ On
8 naddcl ⊢ B ∈ On ∧ C ∈ On → B + C ∈ On
9 8 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C ∈ On
10 ontri1 ⊢ A + C ∈ On ∧ B + C ∈ On → A + C ⊆ B + C ↔ ¬ B + C ∈ A + C
11 7 9 10 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + C ⊆ B + C ↔ ¬ B + C ∈ A + C
12 3 5 11 3bitr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ A + C ⊆ B + C