Metamath Proof Explorer

Theorem nnaord

Description: Ordering property of addition. Proposition 8.4 of TakeutiZaring p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnaord ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nnaordi ⊢ ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
2 1 3adant1 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
3 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) )
4 3 a1i ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 = 𝐵 → ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) ) )
5 nnaordi ⊢ ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐵 ∈ 𝐴 → ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
6 5 3adant2 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐵 ∈ 𝐴 → ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) )
7 4 6 orim12d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) → ( ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) ∨ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) ) )
8 7 con3d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ¬ ( ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) ∨ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
9 df-3an ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐶 ∈ ω ) )
10 ancom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐶 ∈ ω ) ↔ ( 𝐶 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) )
11 anandi ⊢ ( ( 𝐶 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ↔ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ) )
12 9 10 11 3bitri ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ↔ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ) )
13 nnacl ⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐶 +o 𝐴 ) ∈ ω )
14 nnord ⊢ ( ( 𝐶 +o 𝐴 ) ∈ ω → Ord ( 𝐶 +o 𝐴 ) )
15 13 14 syl ⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → Ord ( 𝐶 +o 𝐴 ) )
16 nnacl ⊢ ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 +o 𝐵 ) ∈ ω )
17 nnord ⊢ ( ( 𝐶 +o 𝐵 ) ∈ ω → Ord ( 𝐶 +o 𝐵 ) )
18 16 17 syl ⊢ ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) → Ord ( 𝐶 +o 𝐵 ) )
19 15 18 anim12i ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( Ord ( 𝐶 +o 𝐴 ) ∧ Ord ( 𝐶 +o 𝐵 ) ) )
20 12 19 sylbi ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( Ord ( 𝐶 +o 𝐴 ) ∧ Ord ( 𝐶 +o 𝐵 ) ) )
21 ordtri2 ⊢ ( ( Ord ( 𝐶 +o 𝐴 ) ∧ Ord ( 𝐶 +o 𝐵 ) ) → ( ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ↔ ¬ ( ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) ∨ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) ) )
22 20 21 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ↔ ¬ ( ( 𝐶 +o 𝐴 ) = ( 𝐶 +o 𝐵 ) ∨ ( 𝐶 +o 𝐵 ) ∈ ( 𝐶 +o 𝐴 ) ) ) )
23 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
24 nnord ⊢ ( 𝐵 ∈ ω → Ord 𝐵 )
25 23 24 anim12i ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( Ord 𝐴 ∧ Ord 𝐵 ) )
26 25 3adant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( Ord 𝐴 ∧ Ord 𝐵 ) )
27 ordtri2 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
28 26 27 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
29 8 22 28 3imtr4d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
30 2 29 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )