Metamath Proof Explorer


Theorem nnawordi

Description: Adding to both sides of an inequality in _om . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 12-May-2012)

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

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
2 oveq2 ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
3 1 2 sseq12d ( 𝑥 = ∅ → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) )
4 3 imbi2d ( 𝑥 = ∅ → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ↔ ( 𝐴𝐵 → ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) ) )
5 4 imbi2d ( 𝑥 = ∅ → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) ) ) )
6 oveq2 ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
7 oveq2 ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
8 6 7 sseq12d ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) )
9 8 imbi2d ( 𝑥 = 𝑦 → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ↔ ( 𝐴𝐵 → ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) ) )
10 9 imbi2d ( 𝑥 = 𝑦 → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) ) ) )
11 oveq2 ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
12 oveq2 ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
13 11 12 sseq12d ( 𝑥 = suc 𝑦 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) )
14 13 imbi2d ( 𝑥 = suc 𝑦 → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ↔ ( 𝐴𝐵 → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) )
15 14 imbi2d ( 𝑥 = suc 𝑦 → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) ) )
16 oveq2 ( 𝑥 = 𝐶 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐶 ) )
17 oveq2 ( 𝑥 = 𝐶 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐶 ) )
18 16 17 sseq12d ( 𝑥 = 𝐶 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )
19 18 imbi2d ( 𝑥 = 𝐶 → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ↔ ( 𝐴𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) ) )
20 19 imbi2d ( 𝑥 = 𝐶 → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) ) ) )
21 nnon ( 𝐴 ∈ ω → 𝐴 ∈ On )
22 nnon ( 𝐵 ∈ ω → 𝐵 ∈ On )
23 oa0 ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
24 23 adantr ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o ∅ ) = 𝐴 )
25 oa0 ( 𝐵 ∈ On → ( 𝐵 +o ∅ ) = 𝐵 )
26 25 adantl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o ∅ ) = 𝐵 )
27 24 26 sseq12d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ↔ 𝐴𝐵 ) )
28 27 biimprd ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴𝐵 → ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) )
29 21 22 28 syl2an ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) )
30 nnacl ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o 𝑦 ) ∈ ω )
31 30 ancoms ( ( 𝑦 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐴 +o 𝑦 ) ∈ ω )
32 31 adantrr ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 +o 𝑦 ) ∈ ω )
33 nnon ( ( 𝐴 +o 𝑦 ) ∈ ω → ( 𝐴 +o 𝑦 ) ∈ On )
34 eloni ( ( 𝐴 +o 𝑦 ) ∈ On → Ord ( 𝐴 +o 𝑦 ) )
35 32 33 34 3syl ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → Ord ( 𝐴 +o 𝑦 ) )
36 nnacl ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o 𝑦 ) ∈ ω )
37 36 ancoms ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 +o 𝑦 ) ∈ ω )
38 37 adantrl ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 +o 𝑦 ) ∈ ω )
39 nnon ( ( 𝐵 +o 𝑦 ) ∈ ω → ( 𝐵 +o 𝑦 ) ∈ On )
40 eloni ( ( 𝐵 +o 𝑦 ) ∈ On → Ord ( 𝐵 +o 𝑦 ) )
41 38 39 40 3syl ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → Ord ( 𝐵 +o 𝑦 ) )
42 ordsucsssuc ( ( Ord ( 𝐴 +o 𝑦 ) ∧ Ord ( 𝐵 +o 𝑦 ) ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
43 35 41 42 syl2anc ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
44 43 biimpa ( ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) → suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) )
45 nnasuc ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
46 45 ancoms ( ( 𝑦 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
47 46 adantrr ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
48 nnasuc ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
49 48 ancoms ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
50 49 adantrl ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
51 47 50 sseq12d ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
52 51 adantr ( ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) → ( ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
53 44 52 mpbird ( ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) )
54 53 ex ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) )
55 54 imim2d ( ( 𝑦 ∈ ω ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) → ( 𝐴𝐵 → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) )
56 55 ex ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴𝐵 → ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) → ( 𝐴𝐵 → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) ) )
57 56 a2d ( 𝑦 ∈ ω → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) ) → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) ) )
58 5 10 15 20 29 57 finds ( 𝐶 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) ) )
59 58 com12 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 ∈ ω → ( 𝐴𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) ) )
60 59 3impia ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )