This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐶 ) ) )