Metamath Proof Explorer

Theorem nnaword

Description: Weak ordering property of addition. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnaword ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B ↔ C + 𝑜 A ⊆ C + 𝑜 B

Proof

Step Hyp Ref Expression
1 nnaord ⊢ B ∈ ω ∧ A ∈ ω ∧ C ∈ ω → B ∈ A ↔ C + 𝑜 B ∈ C + 𝑜 A
2 1 3com12 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → B ∈ A ↔ C + 𝑜 B ∈ C + 𝑜 A
3 2 notbid ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → ¬ B ∈ A ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
4 nnord ⊢ A ∈ ω → Ord ⁡ A
5 nnord ⊢ B ∈ ω → Ord ⁡ B
6 ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A
7 4 5 6 syl2an ⊢ A ∈ ω ∧ B ∈ ω → A ⊆ B ↔ ¬ B ∈ A
8 7 3adant3 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B ↔ ¬ B ∈ A
9 nnacl ⊢ C ∈ ω ∧ A ∈ ω → C + 𝑜 A ∈ ω
10 9 ancoms ⊢ A ∈ ω ∧ C ∈ ω → C + 𝑜 A ∈ ω
11 10 3adant2 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 A ∈ ω
12 nnacl ⊢ C ∈ ω ∧ B ∈ ω → C + 𝑜 B ∈ ω
13 12 ancoms ⊢ B ∈ ω ∧ C ∈ ω → C + 𝑜 B ∈ ω
14 13 3adant1 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 B ∈ ω
15 nnord ⊢ C + 𝑜 A ∈ ω → Ord ⁡ C + 𝑜 A
16 nnord ⊢ C + 𝑜 B ∈ ω → Ord ⁡ C + 𝑜 B
17 ordtri1 ⊢ Ord ⁡ C + 𝑜 A ∧ Ord ⁡ C + 𝑜 B → C + 𝑜 A ⊆ C + 𝑜 B ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
18 15 16 17 syl2an ⊢ C + 𝑜 A ∈ ω ∧ C + 𝑜 B ∈ ω → C + 𝑜 A ⊆ C + 𝑜 B ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
19 11 14 18 syl2anc ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → C + 𝑜 A ⊆ C + 𝑜 B ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
20 3 8 19 3bitr4d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⊆ B ↔ C + 𝑜 A ⊆ C + 𝑜 B