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∈xA⋅𝑜y⊆B⋅𝑜y→⋃y∈xA⋅𝑜y⊆⋃y∈xB⋅𝑜y
43 omlim ⊢A∈On∧x∈V∧Lim⁡x→A⋅𝑜x=⋃y∈xA⋅𝑜y
44 43 ad2ant2rl ⊢A∈On∧x∈V∧Lim⁡x∧B∈On∧x∈V∧Lim⁡x→A⋅𝑜x=⋃y∈xA⋅𝑜y
45 omlim ⊢B∈On∧x∈V∧Lim⁡x→B⋅𝑜x=⋃y∈xB⋅𝑜y
46 45 adantl ⊢A∈On∧x∈V∧Lim⁡x∧B∈On∧x∈V∧Lim⁡x→B⋅𝑜x=⋃y∈xB⋅𝑜y
47 44 46 sseq12d ⊢A∈On∧x∈V∧Lim⁡x∧B∈On∧x∈V∧Lim⁡x→A⋅𝑜x⊆B⋅𝑜x↔⋃y∈xA⋅𝑜y⊆⋃y∈xB⋅𝑜y
48 42 47 imbitrrid ⊢A∈On∧x∈V∧Lim⁡x∧B∈On∧x∈V∧Lim⁡x→∀y∈xA⋅𝑜y⊆B⋅𝑜y→A⋅𝑜x⊆B⋅𝑜x
49 48 anandirs ⊢A∈On∧B∈On∧x∈V∧Lim⁡x→∀y∈xA⋅𝑜y⊆B⋅𝑜y→A⋅𝑜x⊆B⋅𝑜x
50 41 49 mpanr1 ⊢A∈On∧B∈On∧Lim⁡x→∀y∈xA⋅𝑜y⊆B⋅𝑜y→A⋅𝑜x⊆B⋅𝑜x
51 50 expcom ⊢Lim⁡x→A∈On∧B∈On→∀y∈xA⋅𝑜y⊆B⋅𝑜y→A⋅𝑜x⊆B⋅𝑜x
52 51 adantrd ⊢Lim⁡x→A∈On∧B∈On∧A⊆B→∀y∈xA⋅𝑜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