Metamath Proof Explorer

Theorem omass

Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of TakeutiZaring p. 65. Theorem 4.4 of Schloeder p. 13. (Contributed by NM, 28-Dec-2004)

Ref Expression
Assertion omass ⊢A∈On∧B∈On∧C∈On→A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C

Proof

Step Hyp Ref Expression
1 oveq2 ⊢x=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜∅
2 oveq2 ⊢x=∅→B⋅𝑜x=B⋅𝑜∅
3 2 oveq2d ⊢x=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜∅
4 1 3 eqeq12d ⊢x=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x↔A⋅𝑜B⋅𝑜∅=A⋅𝑜B⋅𝑜∅
5 oveq2 ⊢x=y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜y
6 oveq2 ⊢x=y→B⋅𝑜x=B⋅𝑜y
7 6 oveq2d ⊢x=y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜y
8 5 7 eqeq12d ⊢x=y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x↔A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y
9 oveq2 ⊢x=suc⁡y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜suc⁡y
10 oveq2 ⊢x=suc⁡y→B⋅𝑜x=B⋅𝑜suc⁡y
11 10 oveq2d ⊢x=suc⁡y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜suc⁡y
12 9 11 eqeq12d ⊢x=suc⁡y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x↔A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y
13 oveq2 ⊢x=C→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜C
14 oveq2 ⊢x=C→B⋅𝑜x=B⋅𝑜C
15 14 oveq2d ⊢x=C→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜C
16 13 15 eqeq12d ⊢x=C→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x↔A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C
17 omcl ⊢A∈On∧B∈On→A⋅𝑜B∈On
18 om0 ⊢A⋅𝑜B∈On→A⋅𝑜B⋅𝑜∅=∅
19 17 18 syl ⊢A∈On∧B∈On→A⋅𝑜B⋅𝑜∅=∅
20 om0 ⊢B∈On→B⋅𝑜∅=∅
21 20 oveq2d ⊢B∈On→A⋅𝑜B⋅𝑜∅=A⋅𝑜∅
22 om0 ⊢A∈On→A⋅𝑜∅=∅
23 21 22 sylan9eqr ⊢A∈On∧B∈On→A⋅𝑜B⋅𝑜∅=∅
24 19 23 eqtr4d ⊢A∈On∧B∈On→A⋅𝑜B⋅𝑜∅=A⋅𝑜B⋅𝑜∅
25 oveq1 ⊢A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
26 omsuc ⊢A⋅𝑜B∈On∧y∈On→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
27 17 26 stoic3 ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
28 omsuc ⊢B∈On∧y∈On→B⋅𝑜suc⁡y=B⋅𝑜y+𝑜B
29 28 3adant1 ⊢A∈On∧B∈On∧y∈On→B⋅𝑜suc⁡y=B⋅𝑜y+𝑜B
30 29 oveq2d ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜y+𝑜B
31 omcl ⊢B∈On∧y∈On→B⋅𝑜y∈On
32 odi ⊢A∈On∧B⋅𝑜y∈On∧B∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
33 31 32 syl3an2 ⊢A∈On∧B∈On∧y∈On∧B∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
34 33 3exp ⊢A∈On→B∈On∧y∈On→B∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
35 34 expd ⊢A∈On→B∈On→y∈On→B∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
36 35 com34 ⊢A∈On→B∈On→B∈On→y∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
37 36 pm2.43d ⊢A∈On→B∈On→y∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
38 37 3imp ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜y+𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
39 30 38 eqtrd ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
40 27 39 eqeq12d ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y↔A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B=A⋅𝑜B⋅𝑜y+𝑜A⋅𝑜B
41 25 40 imbitrrid ⊢A∈On∧B∈On∧y∈On→A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y
42 41 3exp ⊢A∈On→B∈On→y∈On→A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y
43 42 com3r ⊢y∈On→A∈On→B∈On→A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y
44 43 impd ⊢y∈On→A∈On∧B∈On→A⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜suc⁡y=A⋅𝑜B⋅𝑜suc⁡y
45 17 ancoms ⊢B∈On∧A∈On→A⋅𝑜B∈On
46 vex ⊢x∈V
47 omlim ⊢A⋅𝑜B∈On∧x∈V∧Lim⁡x→A⋅𝑜B⋅𝑜x=⋃y∈xA⋅𝑜B⋅𝑜y
48 46 47 mpanr1 ⊢A⋅𝑜B∈On∧Lim⁡x→A⋅𝑜B⋅𝑜x=⋃y∈xA⋅𝑜B⋅𝑜y
49 45 48 sylan ⊢B∈On∧A∈On∧Lim⁡x→A⋅𝑜B⋅𝑜x=⋃y∈xA⋅𝑜B⋅𝑜y
50 49 an32s ⊢B∈On∧Lim⁡x∧A∈On→A⋅𝑜B⋅𝑜x=⋃y∈xA⋅𝑜B⋅𝑜y
51 50 ad2antrr ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B∧∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=⋃y∈xA⋅𝑜B⋅𝑜y
52 iuneq2 ⊢∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→⋃y∈xA⋅𝑜B⋅𝑜y=⋃y∈xA⋅𝑜B⋅𝑜y
53 limelon ⊢x∈V∧Lim⁡x→x∈On
54 46 53 mpan ⊢Lim⁡x→x∈On
55 54 anim1i ⊢Lim⁡x∧B∈On→x∈On∧B∈On
56 55 ancoms ⊢B∈On∧Lim⁡x→x∈On∧B∈On
57 omordi ⊢x∈On∧B∈On∧∅∈B→y∈x→B⋅𝑜y∈B⋅𝑜x
58 56 57 sylan ⊢B∈On∧Lim⁡x∧∅∈B→y∈x→B⋅𝑜y∈B⋅𝑜x
59 ssid ⊢A⋅𝑜B⋅𝑜y⊆A⋅𝑜B⋅𝑜y
60 oveq2 ⊢z=B⋅𝑜y→A⋅𝑜z=A⋅𝑜B⋅𝑜y
61 60 sseq2d ⊢z=B⋅𝑜y→A⋅𝑜B⋅𝑜y⊆A⋅𝑜z↔A⋅𝑜B⋅𝑜y⊆A⋅𝑜B⋅𝑜y
62 61 rspcev ⊢B⋅𝑜y∈B⋅𝑜x∧A⋅𝑜B⋅𝑜y⊆A⋅𝑜B⋅𝑜y→∃z∈B⋅𝑜xA⋅𝑜B⋅𝑜y⊆A⋅𝑜z
63 59 62 mpan2 ⊢B⋅𝑜y∈B⋅𝑜x→∃z∈B⋅𝑜xA⋅𝑜B⋅𝑜y⊆A⋅𝑜z
64 58 63 syl6 ⊢B∈On∧Lim⁡x∧∅∈B→y∈x→∃z∈B⋅𝑜xA⋅𝑜B⋅𝑜y⊆A⋅𝑜z
65 64 ralrimiv ⊢B∈On∧Lim⁡x∧∅∈B→∀y∈x∃z∈B⋅𝑜xA⋅𝑜B⋅𝑜y⊆A⋅𝑜z
66 iunss2 ⊢∀y∈x∃z∈B⋅𝑜xA⋅𝑜B⋅𝑜y⊆A⋅𝑜z→⋃y∈xA⋅𝑜B⋅𝑜y⊆⋃z∈B⋅𝑜xA⋅𝑜z
67 65 66 syl ⊢B∈On∧Lim⁡x∧∅∈B→⋃y∈xA⋅𝑜B⋅𝑜y⊆⋃z∈B⋅𝑜xA⋅𝑜z
68 67 adantlr ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B→⋃y∈xA⋅𝑜B⋅𝑜y⊆⋃z∈B⋅𝑜xA⋅𝑜z
69 omcl ⊢B∈On∧x∈On→B⋅𝑜x∈On
70 54 69 sylan2 ⊢B∈On∧Lim⁡x→B⋅𝑜x∈On
71 onelon ⊢B⋅𝑜x∈On∧z∈B⋅𝑜x→z∈On
72 70 71 sylan ⊢B∈On∧Lim⁡x∧z∈B⋅𝑜x→z∈On
73 72 adantlr ⊢B∈On∧Lim⁡x∧A∈On∧z∈B⋅𝑜x→z∈On
74 omordlim ⊢B∈On∧x∈V∧Lim⁡x∧z∈B⋅𝑜x→∃y∈xz∈B⋅𝑜y
75 74 ex ⊢B∈On∧x∈V∧Lim⁡x→z∈B⋅𝑜x→∃y∈xz∈B⋅𝑜y
76 46 75 mpanr1 ⊢B∈On∧Lim⁡x→z∈B⋅𝑜x→∃y∈xz∈B⋅𝑜y
77 76 ad2antlr ⊢z∈On∧B∈On∧Lim⁡x∧A∈On→z∈B⋅𝑜x→∃y∈xz∈B⋅𝑜y
78 onelon ⊢x∈On∧y∈x→y∈On
79 54 78 sylan ⊢Lim⁡x∧y∈x→y∈On
80 79 31 sylan2 ⊢B∈On∧Lim⁡x∧y∈x→B⋅𝑜y∈On
81 onelss ⊢B⋅𝑜y∈On→z∈B⋅𝑜y→z⊆B⋅𝑜y
82 81 3ad2ant2 ⊢z∈On∧B⋅𝑜y∈On∧A∈On→z∈B⋅𝑜y→z⊆B⋅𝑜y
83 omwordi ⊢z∈On∧B⋅𝑜y∈On∧A∈On→z⊆B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
84 82 83 syld ⊢z∈On∧B⋅𝑜y∈On∧A∈On→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
85 84 3exp ⊢z∈On→B⋅𝑜y∈On→A∈On→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
86 80 85 syl5 ⊢z∈On→B∈On∧Lim⁡x∧y∈x→A∈On→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
87 86 exp4d ⊢z∈On→B∈On→Lim⁡x→y∈x→A∈On→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
88 87 imp32 ⊢z∈On∧B∈On∧Lim⁡x→y∈x→A∈On→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
89 88 com23 ⊢z∈On∧B∈On∧Lim⁡x→A∈On→y∈x→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
90 89 imp ⊢z∈On∧B∈On∧Lim⁡x∧A∈On→y∈x→z∈B⋅𝑜y→A⋅𝑜z⊆A⋅𝑜B⋅𝑜y
91 90 reximdvai ⊢z∈On∧B∈On∧Lim⁡x∧A∈On→∃y∈xz∈B⋅𝑜y→∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
92 77 91 syld ⊢z∈On∧B∈On∧Lim⁡x∧A∈On→z∈B⋅𝑜x→∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
93 92 exp31 ⊢z∈On→B∈On∧Lim⁡x→A∈On→z∈B⋅𝑜x→∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
94 93 imp4c ⊢z∈On→B∈On∧Lim⁡x∧A∈On∧z∈B⋅𝑜x→∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
95 73 94 mpcom ⊢B∈On∧Lim⁡x∧A∈On∧z∈B⋅𝑜x→∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
96 95 ralrimiva ⊢B∈On∧Lim⁡x∧A∈On→∀z∈B⋅𝑜x∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y
97 iunss2 ⊢∀z∈B⋅𝑜x∃y∈xA⋅𝑜z⊆A⋅𝑜B⋅𝑜y→⋃z∈B⋅𝑜xA⋅𝑜z⊆⋃y∈xA⋅𝑜B⋅𝑜y
98 96 97 syl ⊢B∈On∧Lim⁡x∧A∈On→⋃z∈B⋅𝑜xA⋅𝑜z⊆⋃y∈xA⋅𝑜B⋅𝑜y
99 98 adantr ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B→⋃z∈B⋅𝑜xA⋅𝑜z⊆⋃y∈xA⋅𝑜B⋅𝑜y
100 68 99 eqssd ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B→⋃y∈xA⋅𝑜B⋅𝑜y=⋃z∈B⋅𝑜xA⋅𝑜z
101 omlimcl ⊢B∈On∧x∈V∧Lim⁡x∧∅∈B→Lim⁡B⋅𝑜x
102 46 101 mpanlr1 ⊢B∈On∧Lim⁡x∧∅∈B→Lim⁡B⋅𝑜x
103 ovex ⊢B⋅𝑜x∈V
104 omlim ⊢A∈On∧B⋅𝑜x∈V∧Lim⁡B⋅𝑜x→A⋅𝑜B⋅𝑜x=⋃z∈B⋅𝑜xA⋅𝑜z
105 103 104 mpanr1 ⊢A∈On∧Lim⁡B⋅𝑜x→A⋅𝑜B⋅𝑜x=⋃z∈B⋅𝑜xA⋅𝑜z
106 102 105 sylan2 ⊢A∈On∧B∈On∧Lim⁡x∧∅∈B→A⋅𝑜B⋅𝑜x=⋃z∈B⋅𝑜xA⋅𝑜z
107 106 ancoms ⊢B∈On∧Lim⁡x∧∅∈B∧A∈On→A⋅𝑜B⋅𝑜x=⋃z∈B⋅𝑜xA⋅𝑜z
108 107 an32s ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B→A⋅𝑜B⋅𝑜x=⋃z∈B⋅𝑜xA⋅𝑜z
109 100 108 eqtr4d ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B→⋃y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜x
110 52 109 sylan9eqr ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B∧∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→⋃y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜x
111 51 110 eqtrd ⊢B∈On∧Lim⁡x∧A∈On∧∅∈B∧∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
112 111 exp31 ⊢B∈On∧Lim⁡x∧A∈On→∅∈B→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
113 eloni ⊢B∈On→Ord⁡B
114 ord0eln0 ⊢Ord⁡B→∅∈B↔B≠∅
115 114 necon2bbid ⊢Ord⁡B→B=∅↔¬∅∈B
116 113 115 syl ⊢B∈On→B=∅↔¬∅∈B
117 116 ad2antrr ⊢B∈On∧Lim⁡x∧A∈On→B=∅↔¬∅∈B
118 oveq2 ⊢B=∅→A⋅𝑜B=A⋅𝑜∅
119 118 22 sylan9eqr ⊢A∈On∧B=∅→A⋅𝑜B=∅
120 119 oveq1d ⊢A∈On∧B=∅→A⋅𝑜B⋅𝑜x=∅⋅𝑜x
121 om0r ⊢x∈On→∅⋅𝑜x=∅
122 120 121 sylan9eqr ⊢x∈On∧A∈On∧B=∅→A⋅𝑜B⋅𝑜x=∅
123 122 anassrs ⊢x∈On∧A∈On∧B=∅→A⋅𝑜B⋅𝑜x=∅
124 oveq1 ⊢B=∅→B⋅𝑜x=∅⋅𝑜x
125 124 121 sylan9eqr ⊢x∈On∧B=∅→B⋅𝑜x=∅
126 125 oveq2d ⊢x∈On∧B=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜∅
127 126 22 sylan9eq ⊢x∈On∧B=∅∧A∈On→A⋅𝑜B⋅𝑜x=∅
128 127 an32s ⊢x∈On∧A∈On∧B=∅→A⋅𝑜B⋅𝑜x=∅
129 123 128 eqtr4d ⊢x∈On∧A∈On∧B=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
130 129 ex ⊢x∈On∧A∈On→B=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
131 54 130 sylan ⊢Lim⁡x∧A∈On→B=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
132 131 adantll ⊢B∈On∧Lim⁡x∧A∈On→B=∅→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
133 117 132 sylbird ⊢B∈On∧Lim⁡x∧A∈On→¬∅∈B→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
134 133 a1dd ⊢B∈On∧Lim⁡x∧A∈On→¬∅∈B→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
135 112 134 pm2.61d ⊢B∈On∧Lim⁡x∧A∈On→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
136 135 exp31 ⊢B∈On→Lim⁡x→A∈On→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
137 136 com3l ⊢Lim⁡x→A∈On→B∈On→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
138 137 impd ⊢Lim⁡x→A∈On∧B∈On→∀y∈xA⋅𝑜B⋅𝑜y=A⋅𝑜B⋅𝑜y→A⋅𝑜B⋅𝑜x=A⋅𝑜B⋅𝑜x
139 4 8 12 16 24 44 138 tfinds3 ⊢C∈On→A∈On∧B∈On→A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C
140 139 expd ⊢C∈On→A∈On→B∈On→A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C
141 140 com3l ⊢A∈On→B∈On→C∈On→A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C
142 141 3imp ⊢A∈On∧B∈On∧C∈On→A⋅𝑜B⋅𝑜C=A⋅𝑜B⋅𝑜C