Metamath Proof Explorer

Theorem oawordri

Description: Weak ordering property of ordinal addition. Proposition 8.7 of TakeutiZaring p. 59. (Contributed by NM, 7-Dec-2004)

Ref Expression
Assertion oawordri ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
2 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
3 1 2 sseq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ) )
4 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
6 4 5 sseq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ) )
7 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
9 7 8 sseq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐶 ) )
11 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐶 ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )
13 oa0 ⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
14 13 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o ∅ ) = 𝐴 )
15 oa0 ⊢ ( 𝐵 ∈ On → ( 𝐵 +o ∅ ) = 𝐵 )
16 15 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o ∅ ) = 𝐵 )
17 14 16 sseq12d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) ↔ 𝐴 ⊆ 𝐵 ) )
18 17 biimpar ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o ∅ ) ⊆ ( 𝐵 +o ∅ ) )
19 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 +o 𝑦 ) ∈ On )
20 eloni ⊢ ( ( 𝐴 +o 𝑦 ) ∈ On → Ord ( 𝐴 +o 𝑦 ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → Ord ( 𝐴 +o 𝑦 ) )
22 oacl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o 𝑦 ) ∈ On )
23 eloni ⊢ ( ( 𝐵 +o 𝑦 ) ∈ On → Ord ( 𝐵 +o 𝑦 ) )
24 22 23 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → Ord ( 𝐵 +o 𝑦 ) )
25 ordsucsssuc ⊢ ( ( Ord ( 𝐴 +o 𝑦 ) ∧ Ord ( 𝐵 +o 𝑦 ) ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
26 21 24 25 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
27 26 anandirs ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
28 oasuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
29 28 adantlr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
30 oasuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
31 30 adantll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
32 29 31 sseq12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ↔ suc ( 𝐴 +o 𝑦 ) ⊆ suc ( 𝐵 +o 𝑦 ) ) )
33 27 32 bitr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) ↔ ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) )
34 33 biimpd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) )
35 34 expcom ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) )
36 35 adantrd ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o suc 𝑦 ) ⊆ ( 𝐵 +o suc 𝑦 ) ) ) )
37 vex ⊢ 𝑥 ∈ V
38 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
39 oalim ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) )
40 39 adantlr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) )
41 oalim ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐵 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
42 41 adantll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐵 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
43 40 42 sseq12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ↔ ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ) )
44 38 43 syl5ibr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) )
45 37 44 mpanr1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) )
46 45 expcom ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) )
47 46 adantrd ⊢ ( Lim 𝑥 → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ⊆ ( 𝐵 +o 𝑦 ) → ( 𝐴 +o 𝑥 ) ⊆ ( 𝐵 +o 𝑥 ) ) ) )
48 3 6 9 12 18 36 47 tfinds3 ⊢ ( 𝐶 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )
49 48 exp4c ⊢ ( 𝐶 ∈ On → ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) ) ) )
50 49 3imp231 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o 𝐶 ) ⊆ ( 𝐵 +o 𝐶 ) ) )