Metamath Proof Explorer

Theorem omwordri

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of TakeutiZaring p. 63. (Contributed by NM, 20-Dec-2004)

Ref Expression
Assertion omwordri ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = ∅ → A ⋅ 𝑜 x = A ⋅ 𝑜 ∅
2 oveq2 ⊢ x = ∅ → B ⋅ 𝑜 x = B ⋅ 𝑜 ∅
3 1 2 sseq12d ⊢ x = ∅ → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x ↔ A ⋅ 𝑜 ∅ ⊆ B ⋅ 𝑜 ∅
4 oveq2 ⊢ x = y → A ⋅ 𝑜 x = A ⋅ 𝑜 y
5 oveq2 ⊢ x = y → B ⋅ 𝑜 x = B ⋅ 𝑜 y
6 4 5 sseq12d ⊢ x = y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x ↔ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y
7 oveq2 ⊢ x = suc ⁡ y → A ⋅ 𝑜 x = A ⋅ 𝑜 suc ⁡ y
8 oveq2 ⊢ x = suc ⁡ y → B ⋅ 𝑜 x = B ⋅ 𝑜 suc ⁡ y
9 7 8 sseq12d ⊢ x = suc ⁡ y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x ↔ A ⋅ 𝑜 suc ⁡ y ⊆ B ⋅ 𝑜 suc ⁡ y
10 oveq2 ⊢ x = C → A ⋅ 𝑜 x = A ⋅ 𝑜 C
11 oveq2 ⊢ x = C → B ⋅ 𝑜 x = B ⋅ 𝑜 C
12 10 11 sseq12d ⊢ x = C → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x ↔ A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C
13 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
14 0ss ⊢ ∅ ⊆ B ⋅ 𝑜 ∅
15 13 14 eqsstrdi ⊢ A ∈ On → A ⋅ 𝑜 ∅ ⊆ B ⋅ 𝑜 ∅
16 15 ad2antrr ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → A ⋅ 𝑜 ∅ ⊆ B ⋅ 𝑜 ∅
17 omcl ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ∈ On
18 17 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ∈ On
19 omcl ⊢ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 y ∈ On
20 19 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 y ∈ On
21 simp1 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ∈ On
22 oawordri ⊢ A ⋅ 𝑜 y ∈ On ∧ B ⋅ 𝑜 y ∈ On ∧ A ∈ On → A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 A
23 18 20 21 22 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 A
24 23 imp ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 A
25 24 adantrl ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 A
26 oaword ⊢ A ∈ On ∧ B ∈ On ∧ B ⋅ 𝑜 y ∈ On → A ⊆ B ↔ B ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 B
27 20 26 syld3an3 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⊆ B ↔ B ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 B
28 27 biimpa ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B → B ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 B
29 28 adantrr ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → B ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 B
30 25 29 sstrd ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 y + 𝑜 A ⊆ B ⋅ 𝑜 y + 𝑜 B
31 omsuc ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
32 31 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
33 32 adantr ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
34 omsuc ⊢ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
35 34 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
36 35 adantr ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
37 30 33 36 3sstr4d ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On ∧ A ⊆ B ∧ A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 suc ⁡ y ⊆ B ⋅ 𝑜 suc ⁡ y
38 37 exp520 ⊢ A ∈ On → B ∈ On → y ∈ On → A ⊆ B → A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 suc ⁡ y ⊆ B ⋅ 𝑜 suc ⁡ y
39 38 com3r ⊢ y ∈ On → A ∈ On → B ∈ On → A ⊆ B → A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 suc ⁡ y ⊆ B ⋅ 𝑜 suc ⁡ y
40 39 imp4c ⊢ y ∈ On → A ∈ On ∧ B ∈ On ∧ A ⊆ B → A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 suc ⁡ y ⊆ B ⋅ 𝑜 suc ⁡ y
41 vex ⊢ x ∈ V
42 ss2iun ⊢ ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → ⋃ y ∈ x A ⋅ 𝑜 y ⊆ ⋃ y ∈ x B ⋅ 𝑜 y
43 omlim ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 y
44 43 ad2ant2rl ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 y
45 omlim ⊢ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → B ⋅ 𝑜 x = ⋃ y ∈ x B ⋅ 𝑜 y
46 45 adantl ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → B ⋅ 𝑜 x = ⋃ y ∈ x B ⋅ 𝑜 y
47 44 46 sseq12d ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x ↔ ⋃ y ∈ x A ⋅ 𝑜 y ⊆ ⋃ y ∈ x B ⋅ 𝑜 y
48 42 47 imbitrrid ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x
49 48 anandirs ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x
50 41 49 mpanr1 ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x
51 50 expcom ⊢ Lim ⁡ x → A ∈ On ∧ B ∈ On → ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x
52 51 adantrd ⊢ Lim ⁡ x → A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∀ y ∈ x A ⋅ 𝑜 y ⊆ B ⋅ 𝑜 y → A ⋅ 𝑜 x ⊆ B ⋅ 𝑜 x
53 3 6 9 12 16 40 52 tfinds3 ⊢ C ∈ On → A ∈ On ∧ B ∈ On ∧ A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C
54 53 expd ⊢ C ∈ On → A ∈ On ∧ B ∈ On → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C
55 54 3impib ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C
56 55 3coml ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B → A ⋅ 𝑜 C ⊆ B ⋅ 𝑜 C