Metamath Proof Explorer

Theorem omass

Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of TakeutiZaring p. 65. (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 syl5ibr ⊢ 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 ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
48 46 47 mpanr1 ⊢ A ⋅ 𝑜 B ∈ On ∧ Lim ⁡ x → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
49 45 48 sylan ⊢ B ∈ On ∧ A ∈ On ∧ Lim ⁡ x → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
50 49 an32s ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
51 50 ad2antrr ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B ∧ ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
52 iuneq2 ⊢ ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = ⋃ y ∈ x A ⋅ 𝑜 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 ⋅ 𝑜 x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ A ⋅ 𝑜 z
63 59 62 mpan2 ⊢ B ⋅ 𝑜 y ∈ B ⋅ 𝑜 x → ∃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ A ⋅ 𝑜 z
64 58 63 syl6 ⊢ B ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ B → y ∈ x → ∃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ A ⋅ 𝑜 z
65 64 ralrimiv ⊢ B ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ B → ∀ y ∈ x ∃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ A ⋅ 𝑜 z
66 iunss2 ⊢ ∀ y ∈ x ∃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ A ⋅ 𝑜 z → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
67 65 66 syl ⊢ B ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ B → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
68 67 adantlr ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y ⊆ ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 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 ∈ x z ∈ B ⋅ 𝑜 y
75 74 ex ⊢ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → z ∈ B ⋅ 𝑜 x → ∃ y ∈ x z ∈ B ⋅ 𝑜 y
76 46 75 mpanr1 ⊢ B ∈ On ∧ Lim ⁡ x → z ∈ B ⋅ 𝑜 x → ∃ y ∈ x z ∈ B ⋅ 𝑜 y
77 76 ad2antlr ⊢ z ∈ On ∧ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → z ∈ B ⋅ 𝑜 x → ∃ y ∈ x z ∈ 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 ∈ x z ∈ B ⋅ 𝑜 y → ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
92 77 91 syld ⊢ z ∈ On ∧ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → z ∈ B ⋅ 𝑜 x → ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
93 92 exp31 ⊢ z ∈ On → B ∈ On ∧ Lim ⁡ x → A ∈ On → z ∈ B ⋅ 𝑜 x → ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
94 93 imp4c ⊢ z ∈ On → B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ z ∈ B ⋅ 𝑜 x → ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
95 73 94 mpcom ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ z ∈ B ⋅ 𝑜 x → ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
96 95 ralrimiva ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → ∀ z ∈ B ⋅ 𝑜 x ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y
97 iunss2 ⊢ ∀ z ∈ B ⋅ 𝑜 x ∃ y ∈ x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B ⋅ 𝑜 y → ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
98 96 97 syl ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
99 98 adantr ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B → ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y
100 68 99 eqssd ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 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 ⋅ 𝑜 x A ⋅ 𝑜 z
105 103 104 mpanr1 ⊢ A ∈ On ∧ Lim ⁡ B ⋅ 𝑜 x → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
106 102 105 sylan2 ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ B → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
107 106 ancoms ⊢ B ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ B ∧ A ∈ On → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
108 107 an32s ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B → A ⋅ 𝑜 B ⋅ 𝑜 x = ⋃ z ∈ B ⋅ 𝑜 x A ⋅ 𝑜 z
109 100 108 eqtr4d ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 x
110 52 109 sylan9eqr ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B ∧ ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → ⋃ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 x
111 51 110 eqtrd ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ B ∧ ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
112 111 exp31 ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → ∅ ∈ B → ∀ y ∈ x A ⋅ 𝑜 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 ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
135 112 134 pm2.61d ⊢ B ∈ On ∧ Lim ⁡ x ∧ A ∈ On → ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
136 135 exp31 ⊢ B ∈ On → Lim ⁡ x → A ∈ On → ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
137 136 com3l ⊢ Lim ⁡ x → A ∈ On → B ∈ On → ∀ y ∈ x A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
138 137 impd ⊢ Lim ⁡ x → A ∈ On ∧ B ∈ On → ∀ y ∈ x A ⋅ 𝑜 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