Metamath Proof Explorer

Theorem nnaordi

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

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

Proof

Step Hyp Ref Expression
1 elnn ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝐴 ∈ ω )
2 1 ancoms ⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ω )
3 2 adantll ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ω )
4 nnord ⊢ ( 𝐵 ∈ ω → Ord 𝐵 )
5 ordsucss ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
6 4 5 syl ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
7 6 ad2antlr ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ ω ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
8 peano2b ⊢ ( 𝐴 ∈ ω ↔ suc 𝐴 ∈ ω )
9 oveq2 ⊢ ( 𝑥 = suc 𝐴 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝐴 ) )
10 9 sseq2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) )
11 10 imbi2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) ) )
12 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝑦 ) )
13 12 sseq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) ) )
15 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o suc 𝑦 ) )
16 15 sseq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) )
17 16 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
18 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o 𝐵 ) )
19 18 sseq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑥 ) ) ↔ ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) )
21 ssid ⊢ ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 )
22 21 2a1i ⊢ ( suc 𝐴 ∈ ω → ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝐴 ) ) )
23 sssucid ⊢ ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 )
24 sstr2 ⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( ( 𝐶 +o 𝑦 ) ⊆ suc ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) )
25 23 24 mpi ⊢ ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) )
26 nnasuc ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) )
27 26 ancoms ⊢ ( ( 𝑦 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 +o suc 𝑦 ) = suc ( 𝐶 +o 𝑦 ) )
28 27 sseq2d ⊢ ( ( 𝑦 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ↔ ( 𝐶 +o suc 𝐴 ) ⊆ suc ( 𝐶 +o 𝑦 ) ) )
29 25 28 syl5ibr ⊢ ( ( 𝑦 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) )
30 29 ex ⊢ ( 𝑦 ∈ ω → ( 𝐶 ∈ ω → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
31 30 ad2antrr ⊢ ( ( ( 𝑦 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( 𝐶 ∈ ω → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
32 31 a2d ⊢ ( ( ( 𝑦 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝑦 ) ) → ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o suc 𝑦 ) ) ) )
33 11 14 17 20 22 32 findsg ⊢ ( ( ( 𝐵 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴 ⊆ 𝐵 ) → ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
34 33 exp31 ⊢ ( 𝐵 ∈ ω → ( suc 𝐴 ∈ ω → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
35 8 34 syl5bi ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ ω → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
36 35 com4r ⊢ ( 𝐶 ∈ ω → ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) ) ) )
37 36 imp31 ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ ω ) → ( suc 𝐴 ⊆ 𝐵 → ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
38 nnasuc ⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐶 +o suc 𝐴 ) = suc ( 𝐶 +o 𝐴 ) )
39 38 sseq1d ⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ↔ suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) ) )
40 ovex ⊢ ( 𝐶 +o 𝐴 ) ∈ V
41 sucssel ⊢ ( ( 𝐶 +o 𝐴 ) ∈ V → ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
42 40 41 ax-mp ⊢ ( suc ( 𝐶 +o 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
43 39 42 syl6bi ⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
44 43 adantlr ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ ω ) → ( ( 𝐶 +o suc 𝐴 ) ⊆ ( 𝐶 +o 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
45 7 37 44 3syld ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
46 45 imp ⊢ ( ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ ω ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
47 46 an32s ⊢ ( ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ 𝐵 ) ∧ 𝐴 ∈ ω ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
48 3 47 mpdan ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) )
49 48 ex ⊢ ( ( 𝐶 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
50 49 ancoms ⊢ ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )