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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )

Proof

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