Metamath Proof Explorer

Theorem odi

Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of TakeutiZaring p. 64. (Contributed by NM, 26-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = ∅ → B + 𝑜 x = B + 𝑜 ∅
2 1 oveq2d ⊢ x = ∅ → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 ∅
3 oveq2 ⊢ x = ∅ → A ⋅ 𝑜 x = A ⋅ 𝑜 ∅
4 3 oveq2d ⊢ x = ∅ → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 ∅
5 2 4 eqeq12d ⊢ x = ∅ → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x ↔ A ⋅ 𝑜 B + 𝑜 ∅ = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 ∅
6 oveq2 ⊢ x = y → B + 𝑜 x = B + 𝑜 y
7 6 oveq2d ⊢ x = y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 y
8 oveq2 ⊢ x = y → A ⋅ 𝑜 x = A ⋅ 𝑜 y
9 8 oveq2d ⊢ x = y → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y
10 7 9 eqeq12d ⊢ x = y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x ↔ A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y
11 oveq2 ⊢ x = suc ⁡ y → B + 𝑜 x = B + 𝑜 suc ⁡ y
12 11 oveq2d ⊢ x = suc ⁡ y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 suc ⁡ y
13 oveq2 ⊢ x = suc ⁡ y → A ⋅ 𝑜 x = A ⋅ 𝑜 suc ⁡ y
14 13 oveq2d ⊢ x = suc ⁡ y → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
15 12 14 eqeq12d ⊢ x = suc ⁡ y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x ↔ A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
16 oveq2 ⊢ x = C → B + 𝑜 x = B + 𝑜 C
17 16 oveq2d ⊢ x = C → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 C
18 oveq2 ⊢ x = C → A ⋅ 𝑜 x = A ⋅ 𝑜 C
19 18 oveq2d ⊢ x = C → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C
20 17 19 eqeq12d ⊢ x = C → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x ↔ A ⋅ 𝑜 B + 𝑜 C = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C
21 omcl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On
22 oa0 ⊢ A ⋅ 𝑜 B ∈ On → A ⋅ 𝑜 B + 𝑜 ∅ = A ⋅ 𝑜 B
23 21 22 syl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 ∅ = A ⋅ 𝑜 B
24 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
25 24 adantr ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 ∅ = ∅
26 25 oveq2d ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 ∅ = A ⋅ 𝑜 B + 𝑜 ∅
27 oa0 ⊢ B ∈ On → B + 𝑜 ∅ = B
28 27 adantl ⊢ A ∈ On ∧ B ∈ On → B + 𝑜 ∅ = B
29 28 oveq2d ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 ∅ = A ⋅ 𝑜 B
30 23 26 29 3eqtr4rd ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 ∅ = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 ∅
31 oveq1 ⊢ A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
32 oasuc ⊢ B ∈ On ∧ y ∈ On → B + 𝑜 suc ⁡ y = suc ⁡ B + 𝑜 y
33 32 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → B + 𝑜 suc ⁡ y = suc ⁡ B + 𝑜 y
34 33 oveq2d ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 suc ⁡ B + 𝑜 y
35 oacl ⊢ B ∈ On ∧ y ∈ On → B + 𝑜 y ∈ On
36 omsuc ⊢ A ∈ On ∧ B + 𝑜 y ∈ On → A ⋅ 𝑜 suc ⁡ B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 y + 𝑜 A
37 35 36 sylan2 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 y + 𝑜 A
38 37 3impb ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 y + 𝑜 A
39 34 38 eqtrd ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 y + 𝑜 A
40 omsuc ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
41 40 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
42 41 oveq2d ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
43 omcl ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ∈ On
44 oaass ⊢ A ⋅ 𝑜 B ∈ On ∧ A ⋅ 𝑜 y ∈ On ∧ A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
45 21 44 syl3an1 ⊢ A ∈ On ∧ B ∈ On ∧ A ⋅ 𝑜 y ∈ On ∧ A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
46 43 45 syl3an2 ⊢ A ∈ On ∧ B ∈ On ∧ A ∈ On ∧ y ∈ On ∧ A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
47 46 3exp ⊢ A ∈ On ∧ B ∈ On → A ∈ On ∧ y ∈ On → A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
48 47 exp4b ⊢ A ∈ On → B ∈ On → A ∈ On → y ∈ On → A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
49 48 pm2.43a ⊢ A ∈ On → B ∈ On → y ∈ On → A ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
50 49 com4r ⊢ A ∈ On → A ∈ On → B ∈ On → y ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
51 50 pm2.43i ⊢ A ∈ On → B ∈ On → y ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
52 51 3imp ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
53 42 52 eqtr4d ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
54 39 53 eqeq12d ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y ↔ A ⋅ 𝑜 B + 𝑜 y + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y + 𝑜 A
55 31 54 syl5ibr ⊢ A ∈ On ∧ B ∈ On ∧ y ∈ On → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
56 55 3exp ⊢ A ∈ On → B ∈ On → y ∈ On → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
57 56 com3r ⊢ y ∈ On → A ∈ On → B ∈ On → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
58 57 impd ⊢ y ∈ On → A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 suc ⁡ y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 suc ⁡ y
59 vex ⊢ x ∈ V
60 limelon ⊢ x ∈ V ∧ Lim ⁡ x → x ∈ On
61 59 60 mpan ⊢ Lim ⁡ x → x ∈ On
62 oacl ⊢ B ∈ On ∧ x ∈ On → B + 𝑜 x ∈ On
63 om0r ⊢ B + 𝑜 x ∈ On → ∅ ⋅ 𝑜 B + 𝑜 x = ∅
64 62 63 syl ⊢ B ∈ On ∧ x ∈ On → ∅ ⋅ 𝑜 B + 𝑜 x = ∅
65 om0r ⊢ B ∈ On → ∅ ⋅ 𝑜 B = ∅
66 om0r ⊢ x ∈ On → ∅ ⋅ 𝑜 x = ∅
67 65 66 oveqan12d ⊢ B ∈ On ∧ x ∈ On → ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x = ∅ + 𝑜 ∅
68 0elon ⊢ ∅ ∈ On
69 oa0 ⊢ ∅ ∈ On → ∅ + 𝑜 ∅ = ∅
70 68 69 ax-mp ⊢ ∅ + 𝑜 ∅ = ∅
71 67 70 eqtr2di ⊢ B ∈ On ∧ x ∈ On → ∅ = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
72 64 71 eqtrd ⊢ B ∈ On ∧ x ∈ On → ∅ ⋅ 𝑜 B + 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
73 61 72 sylan2 ⊢ B ∈ On ∧ Lim ⁡ x → ∅ ⋅ 𝑜 B + 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
74 73 ancoms ⊢ Lim ⁡ x ∧ B ∈ On → ∅ ⋅ 𝑜 B + 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
75 oveq1 ⊢ A = ∅ → A ⋅ 𝑜 B + 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 x
76 oveq1 ⊢ A = ∅ → A ⋅ 𝑜 B = ∅ ⋅ 𝑜 B
77 oveq1 ⊢ A = ∅ → A ⋅ 𝑜 x = ∅ ⋅ 𝑜 x
78 76 77 oveq12d ⊢ A = ∅ → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
79 75 78 eqeq12d ⊢ A = ∅ → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x ↔ ∅ ⋅ 𝑜 B + 𝑜 x = ∅ ⋅ 𝑜 B + 𝑜 ∅ ⋅ 𝑜 x
80 74 79 syl5ibr ⊢ A = ∅ → Lim ⁡ x ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
81 80 expd ⊢ A = ∅ → Lim ⁡ x → B ∈ On → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
82 81 com3r ⊢ B ∈ On → A = ∅ → Lim ⁡ x → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
83 82 imp ⊢ B ∈ On ∧ A = ∅ → Lim ⁡ x → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
84 83 a1dd ⊢ B ∈ On ∧ A = ∅ → Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
85 simplr ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → B ∈ On
86 62 ancoms ⊢ x ∈ On ∧ B ∈ On → B + 𝑜 x ∈ On
87 onelon ⊢ B + 𝑜 x ∈ On ∧ z ∈ B + 𝑜 x → z ∈ On
88 86 87 sylan ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → z ∈ On
89 ontri1 ⊢ B ∈ On ∧ z ∈ On → B ⊆ z ↔ ¬ z ∈ B
90 oawordex ⊢ B ∈ On ∧ z ∈ On → B ⊆ z ↔ ∃ v ∈ On B + 𝑜 v = z
91 89 90 bitr3d ⊢ B ∈ On ∧ z ∈ On → ¬ z ∈ B ↔ ∃ v ∈ On B + 𝑜 v = z
92 85 88 91 syl2anc ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → ¬ z ∈ B ↔ ∃ v ∈ On B + 𝑜 v = z
93 oaord ⊢ v ∈ On ∧ x ∈ On ∧ B ∈ On → v ∈ x ↔ B + 𝑜 v ∈ B + 𝑜 x
94 93 3expb ⊢ v ∈ On ∧ x ∈ On ∧ B ∈ On → v ∈ x ↔ B + 𝑜 v ∈ B + 𝑜 x
95 eleq1 ⊢ B + 𝑜 v = z → B + 𝑜 v ∈ B + 𝑜 x ↔ z ∈ B + 𝑜 x
96 94 95 sylan9bb ⊢ v ∈ On ∧ x ∈ On ∧ B ∈ On ∧ B + 𝑜 v = z → v ∈ x ↔ z ∈ B + 𝑜 x
97 iba ⊢ B + 𝑜 v = z → v ∈ x ↔ v ∈ x ∧ B + 𝑜 v = z
98 97 adantl ⊢ v ∈ On ∧ x ∈ On ∧ B ∈ On ∧ B + 𝑜 v = z → v ∈ x ↔ v ∈ x ∧ B + 𝑜 v = z
99 96 98 bitr3d ⊢ v ∈ On ∧ x ∈ On ∧ B ∈ On ∧ B + 𝑜 v = z → z ∈ B + 𝑜 x ↔ v ∈ x ∧ B + 𝑜 v = z
100 99 an32s ⊢ v ∈ On ∧ B + 𝑜 v = z ∧ x ∈ On ∧ B ∈ On → z ∈ B + 𝑜 x ↔ v ∈ x ∧ B + 𝑜 v = z
101 100 biimpcd ⊢ z ∈ B + 𝑜 x → v ∈ On ∧ B + 𝑜 v = z ∧ x ∈ On ∧ B ∈ On → v ∈ x ∧ B + 𝑜 v = z
102 101 exp4c ⊢ z ∈ B + 𝑜 x → v ∈ On → B + 𝑜 v = z → x ∈ On ∧ B ∈ On → v ∈ x ∧ B + 𝑜 v = z
103 102 com4r ⊢ x ∈ On ∧ B ∈ On → z ∈ B + 𝑜 x → v ∈ On → B + 𝑜 v = z → v ∈ x ∧ B + 𝑜 v = z
104 103 imp ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → v ∈ On → B + 𝑜 v = z → v ∈ x ∧ B + 𝑜 v = z
105 104 reximdvai ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → ∃ v ∈ On B + 𝑜 v = z → ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
106 92 105 sylbid ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → ¬ z ∈ B → ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
107 106 orrd ⊢ x ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
108 61 107 sylanl1 ⊢ Lim ⁡ x ∧ B ∈ On ∧ z ∈ B + 𝑜 x → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
109 108 adantlrl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ z ∈ B + 𝑜 x → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
110 109 adantlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ z ∈ B + 𝑜 x → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z
111 0ellim ⊢ Lim ⁡ x → ∅ ∈ x
112 om00el ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ A ⋅ 𝑜 x ↔ ∅ ∈ A ∧ ∅ ∈ x
113 112 biimprd ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ A ∧ ∅ ∈ x → ∅ ∈ A ⋅ 𝑜 x
114 111 113 sylan2i ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ A ∧ Lim ⁡ x → ∅ ∈ A ⋅ 𝑜 x
115 61 114 sylan2 ⊢ A ∈ On ∧ Lim ⁡ x → ∅ ∈ A ∧ Lim ⁡ x → ∅ ∈ A ⋅ 𝑜 x
116 115 exp4b ⊢ A ∈ On → Lim ⁡ x → ∅ ∈ A → Lim ⁡ x → ∅ ∈ A ⋅ 𝑜 x
117 116 com4r ⊢ Lim ⁡ x → A ∈ On → Lim ⁡ x → ∅ ∈ A → ∅ ∈ A ⋅ 𝑜 x
118 117 pm2.43a ⊢ Lim ⁡ x → A ∈ On → ∅ ∈ A → ∅ ∈ A ⋅ 𝑜 x
119 118 imp31 ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A → ∅ ∈ A ⋅ 𝑜 x
120 119 a1d ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A → z ∈ B → ∅ ∈ A ⋅ 𝑜 x
121 120 adantlrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → ∅ ∈ A ⋅ 𝑜 x
122 omordi ⊢ B ∈ On ∧ A ∈ On ∧ ∅ ∈ A → z ∈ B → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B
123 122 ancom1s ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B
124 onelss ⊢ A ⋅ 𝑜 B ∈ On → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B
125 22 sseq2d ⊢ A ⋅ 𝑜 B ∈ On → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅ ↔ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B
126 124 125 sylibrd ⊢ A ⋅ 𝑜 B ∈ On → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
127 21 126 syl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
128 127 adantr ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 z ∈ A ⋅ 𝑜 B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
129 123 128 syld ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
130 129 adantll ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
131 121 130 jcad ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → ∅ ∈ A ⋅ 𝑜 x ∧ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
132 oveq2 ⊢ w = ∅ → A ⋅ 𝑜 B + 𝑜 w = A ⋅ 𝑜 B + 𝑜 ∅
133 132 sseq2d ⊢ w = ∅ → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w ↔ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅
134 133 rspcev ⊢ ∅ ∈ A ⋅ 𝑜 x ∧ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 ∅ → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
135 131 134 syl6 ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → z ∈ B → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
136 135 adantrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → z ∈ B → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
137 omordi ⊢ x ∈ On ∧ A ∈ On ∧ ∅ ∈ A → v ∈ x → A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x
138 61 137 sylanl1 ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A → v ∈ x → A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x
139 138 adantrd ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x
140 139 adantrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x
141 oveq2 ⊢ y = v → B + 𝑜 y = B + 𝑜 v
142 141 oveq2d ⊢ y = v → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 v
143 oveq2 ⊢ y = v → A ⋅ 𝑜 y = A ⋅ 𝑜 v
144 143 oveq2d ⊢ y = v → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
145 142 144 eqeq12d ⊢ y = v → A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ↔ A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
146 145 rspccv ⊢ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
147 oveq2 ⊢ B + 𝑜 v = z → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 z
148 eqeq1 ⊢ A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 z ↔ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v = A ⋅ 𝑜 z
149 147 148 syl5ib ⊢ A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → B + 𝑜 v = z → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v = A ⋅ 𝑜 z
150 eqimss2 ⊢ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v = A ⋅ 𝑜 z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
151 149 150 syl6 ⊢ A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → B + 𝑜 v = z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
152 151 imim2i ⊢ v ∈ x → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → v ∈ x → B + 𝑜 v = z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
153 152 impd ⊢ v ∈ x → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
154 146 153 syl ⊢ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
155 154 ad2antll ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
156 140 155 jcad ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x ∧ B + 𝑜 v = z → A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x ∧ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
157 oveq2 ⊢ w = A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
158 157 sseq2d ⊢ w = A ⋅ 𝑜 v → A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w ↔ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
159 158 rspcev ⊢ A ⋅ 𝑜 v ∈ A ⋅ 𝑜 x ∧ A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
160 156 159 syl6 ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → v ∈ x ∧ B + 𝑜 v = z → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
161 160 rexlimdvw ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
162 161 adantlrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
163 136 162 jaod ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
164 163 adantr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ z ∈ B + 𝑜 x → z ∈ B ∨ ∃ v ∈ On v ∈ x ∧ B + 𝑜 v = z → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
165 110 164 mpd ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ z ∈ B + 𝑜 x → ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
166 165 ralrimiva ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ∀ z ∈ B + 𝑜 x ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w
167 iunss2 ⊢ ∀ z ∈ B + 𝑜 x ∃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 z ⊆ A ⋅ 𝑜 B + 𝑜 w → ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z ⊆ ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
168 166 167 syl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z ⊆ ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
169 omordlim ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
170 169 ex ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x → w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
171 59 170 mpanr1 ⊢ A ∈ On ∧ Lim ⁡ x → w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
172 171 ancoms ⊢ Lim ⁡ x ∧ A ∈ On → w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
173 172 imp ⊢ Lim ⁡ x ∧ A ∈ On ∧ w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
174 173 adantlrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
175 174 adantlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v
176 oaordi ⊢ x ∈ On ∧ B ∈ On → v ∈ x → B + 𝑜 v ∈ B + 𝑜 x
177 61 176 sylan ⊢ Lim ⁡ x ∧ B ∈ On → v ∈ x → B + 𝑜 v ∈ B + 𝑜 x
178 177 imp ⊢ Lim ⁡ x ∧ B ∈ On ∧ v ∈ x → B + 𝑜 v ∈ B + 𝑜 x
179 178 adantlrl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ v ∈ x → B + 𝑜 v ∈ B + 𝑜 x
180 179 a1d ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → B + 𝑜 v ∈ B + 𝑜 x
181 180 adantlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → B + 𝑜 v ∈ B + 𝑜 x
182 limord ⊢ Lim ⁡ x → Ord ⁡ x
183 ordelon ⊢ Ord ⁡ x ∧ v ∈ x → v ∈ On
184 182 183 sylan ⊢ Lim ⁡ x ∧ v ∈ x → v ∈ On
185 omcl ⊢ A ∈ On ∧ v ∈ On → A ⋅ 𝑜 v ∈ On
186 185 ancoms ⊢ v ∈ On ∧ A ∈ On → A ⋅ 𝑜 v ∈ On
187 186 adantrr ⊢ v ∈ On ∧ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 v ∈ On
188 21 adantl ⊢ v ∈ On ∧ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On
189 oaordi ⊢ A ⋅ 𝑜 v ∈ On ∧ A ⋅ 𝑜 B ∈ On → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
190 187 188 189 syl2anc ⊢ v ∈ On ∧ A ∈ On ∧ B ∈ On → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
191 184 190 sylan ⊢ Lim ⁡ x ∧ v ∈ x ∧ A ∈ On ∧ B ∈ On → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
192 191 an32s ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
193 192 adantlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
194 145 rspccva ⊢ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 v = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
195 194 eleq2d ⊢ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v ↔ A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
196 195 adantll ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v ↔ A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 v
197 193 196 sylibrd ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v
198 oacl ⊢ B ∈ On ∧ v ∈ On → B + 𝑜 v ∈ On
199 198 ancoms ⊢ v ∈ On ∧ B ∈ On → B + 𝑜 v ∈ On
200 omcl ⊢ A ∈ On ∧ B + 𝑜 v ∈ On → A ⋅ 𝑜 B + 𝑜 v ∈ On
201 199 200 sylan2 ⊢ A ∈ On ∧ v ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 v ∈ On
202 201 an12s ⊢ v ∈ On ∧ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 v ∈ On
203 184 202 sylan ⊢ Lim ⁡ x ∧ v ∈ x ∧ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 v ∈ On
204 203 an32s ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 v ∈ On
205 onelss ⊢ A ⋅ 𝑜 B + 𝑜 v ∈ On → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
206 204 205 syl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
207 206 adantlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → A ⋅ 𝑜 B + 𝑜 w ∈ A ⋅ 𝑜 B + 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
208 197 207 syld ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
209 181 208 jcad ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → B + 𝑜 v ∈ B + 𝑜 x ∧ A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
210 oveq2 ⊢ z = B + 𝑜 v → A ⋅ 𝑜 z = A ⋅ 𝑜 B + 𝑜 v
211 210 sseq2d ⊢ z = B + 𝑜 v → A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z ↔ A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v
212 211 rspcev ⊢ B + 𝑜 v ∈ B + 𝑜 x ∧ A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 B + 𝑜 v → ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
213 209 212 syl6 ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ v ∈ x → w ∈ A ⋅ 𝑜 v → ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
214 213 rexlimdva ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ∃ v ∈ x w ∈ A ⋅ 𝑜 v → ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
215 214 adantr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ w ∈ A ⋅ 𝑜 x → ∃ v ∈ x w ∈ A ⋅ 𝑜 v → ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
216 175 215 mpd ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y ∧ w ∈ A ⋅ 𝑜 x → ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
217 216 ralrimiva ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ∀ w ∈ A ⋅ 𝑜 x ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z
218 iunss2 ⊢ ∀ w ∈ A ⋅ 𝑜 x ∃ z ∈ B + 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ A ⋅ 𝑜 z → ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
219 217 218 syl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
220 219 adantrl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w ⊆ ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
221 168 220 eqssd ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z = ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
222 oalimcl ⊢ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → Lim ⁡ B + 𝑜 x
223 59 222 mpanr1 ⊢ B ∈ On ∧ Lim ⁡ x → Lim ⁡ B + 𝑜 x
224 223 ancoms ⊢ Lim ⁡ x ∧ B ∈ On → Lim ⁡ B + 𝑜 x
225 224 anim2i ⊢ A ∈ On ∧ Lim ⁡ x ∧ B ∈ On → A ∈ On ∧ Lim ⁡ B + 𝑜 x
226 225 an12s ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On → A ∈ On ∧ Lim ⁡ B + 𝑜 x
227 ovex ⊢ B + 𝑜 x ∈ V
228 omlim ⊢ A ∈ On ∧ B + 𝑜 x ∈ V ∧ Lim ⁡ B + 𝑜 x → A ⋅ 𝑜 B + 𝑜 x = ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
229 227 228 mpanr1 ⊢ A ∈ On ∧ Lim ⁡ B + 𝑜 x → A ⋅ 𝑜 B + 𝑜 x = ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
230 226 229 syl ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 x = ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
231 230 adantr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = ⋃ z ∈ B + 𝑜 x A ⋅ 𝑜 z
232 21 ad2antlr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 B ∈ On
233 59 jctl ⊢ Lim ⁡ x → x ∈ V ∧ Lim ⁡ x
234 233 anim1ci ⊢ Lim ⁡ x ∧ A ∈ On → A ∈ On ∧ x ∈ V ∧ Lim ⁡ x
235 omlimcl ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ ∅ ∈ A → Lim ⁡ A ⋅ 𝑜 x
236 234 235 sylan ⊢ Lim ⁡ x ∧ A ∈ On ∧ ∅ ∈ A → Lim ⁡ A ⋅ 𝑜 x
237 236 adantlrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → Lim ⁡ A ⋅ 𝑜 x
238 ovex ⊢ A ⋅ 𝑜 x ∈ V
239 237 238 jctil ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 x ∈ V ∧ Lim ⁡ A ⋅ 𝑜 x
240 oalim ⊢ A ⋅ 𝑜 B ∈ On ∧ A ⋅ 𝑜 x ∈ V ∧ Lim ⁡ A ⋅ 𝑜 x → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
241 232 239 240 syl2anc ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
242 241 adantrr ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x = ⋃ w ∈ A ⋅ 𝑜 x A ⋅ 𝑜 B + 𝑜 w
243 221 231 242 3eqtr4d ⊢ Lim ⁡ x ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
244 243 exp43 ⊢ Lim ⁡ x → A ∈ On ∧ B ∈ On → ∅ ∈ A → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
245 244 com3l ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A → Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
246 245 imp ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
247 84 246 oe0lem ⊢ A ∈ On ∧ B ∈ On → Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
248 247 com12 ⊢ Lim ⁡ x → A ∈ On ∧ B ∈ On → ∀ y ∈ x A ⋅ 𝑜 B + 𝑜 y = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 y → A ⋅ 𝑜 B + 𝑜 x = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 x
249 5 10 15 20 30 58 248 tfinds3 ⊢ C ∈ On → A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 C = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C
250 249 expdcom ⊢ A ∈ On → B ∈ On → C ∈ On → A ⋅ 𝑜 B + 𝑜 C = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C
251 250 3imp ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⋅ 𝑜 B + 𝑜 C = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C