Metamath Proof Explorer

Theorem odi

Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of TakeutiZaring p. 64. Theorem 4.3 of Schloeder p. 12. (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 imbitrrid ⊢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 imbitrrid ⊢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∈xA⋅𝑜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∈OnB+𝑜v=z
91 89 90 bitr3d ⊢B∈On∧z∈On→¬z∈B↔∃v∈OnB+𝑜v=z
92 85 88 91 syl2anc ⊢x∈On∧B∈On∧z∈B+𝑜x→¬z∈B↔∃v∈OnB+𝑜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∈OnB+𝑜v=z→∃v∈Onv∈x∧B+𝑜v=z
106 92 105 sylbid ⊢x∈On∧B∈On∧z∈B+𝑜x→¬z∈B→∃v∈Onv∈x∧B+𝑜v=z
107 106 orrd ⊢x∈On∧B∈On∧z∈B+𝑜x→z∈B∨∃v∈Onv∈x∧B+𝑜v=z
108 61 107 sylanl1 ⊢Lim⁡x∧B∈On∧z∈B+𝑜x→z∈B∨∃v∈Onv∈x∧B+𝑜v=z
109 108 adantlrl ⊢Lim⁡x∧A∈On∧B∈On∧z∈B+𝑜x→z∈B∨∃v∈Onv∈x∧B+𝑜v=z
110 109 adantlr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧z∈B+𝑜x→z∈B∨∃v∈Onv∈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⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
135 131 134 syl6 ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A→z∈B→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
136 135 adantrr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→z∈B→∃w∈A⋅𝑜xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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 imbitrid ⊢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∈xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
160 156 159 syl6 ⊢Lim⁡x∧A∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→v∈x∧B+𝑜v=z→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
161 160 rexlimdvw ⊢Lim⁡x∧A∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→∃v∈Onv∈x∧B+𝑜v=z→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
162 161 adantlrr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→∃v∈Onv∈x∧B+𝑜v=z→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
163 136 162 jaod ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→z∈B∨∃v∈Onv∈x∧B+𝑜v=z→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
164 163 adantr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧z∈B+𝑜x→z∈B∨∃v∈Onv∈x∧B+𝑜v=z→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
165 110 164 mpd ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧z∈B+𝑜x→∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
166 165 ralrimiva ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→∀z∈B+𝑜x∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w
167 iunss2 ⊢∀z∈B+𝑜x∃w∈A⋅𝑜xA⋅𝑜z⊆A⋅𝑜B+𝑜w→⋃z∈B+𝑜xA⋅𝑜z⊆⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w
168 166 167 syl ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→⋃z∈B+𝑜xA⋅𝑜z⊆⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w
169 omordlim ⊢A∈On∧x∈V∧Lim⁡x∧w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
170 169 ex ⊢A∈On∧x∈V∧Lim⁡x→w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
171 59 170 mpanr1 ⊢A∈On∧Lim⁡x→w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
172 171 ancoms ⊢Lim⁡x∧A∈On→w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
173 172 imp ⊢Lim⁡x∧A∈On∧w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
174 173 adantlrr ⊢Lim⁡x∧A∈On∧B∈On∧w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v
175 174 adantlr ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧w∈A⋅𝑜x→∃v∈xw∈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∈xA⋅𝑜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∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧v∈x→w∈A⋅𝑜v→A⋅𝑜B+𝑜w∈A⋅𝑜B+𝑜A⋅𝑜v
194 145 rspccva ⊢∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧v∈x→A⋅𝑜B+𝑜v=A⋅𝑜B+𝑜A⋅𝑜v
195 194 eleq2d ⊢∀y∈xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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∈xA⋅𝑜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+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
213 209 212 syl6 ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧v∈x→w∈A⋅𝑜v→∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
214 213 rexlimdva ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→∃v∈xw∈A⋅𝑜v→∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
215 214 adantr ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧w∈A⋅𝑜x→∃v∈xw∈A⋅𝑜v→∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
216 175 215 mpd ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y∧w∈A⋅𝑜x→∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
217 216 ralrimiva ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→∀w∈A⋅𝑜x∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z
218 iunss2 ⊢∀w∈A⋅𝑜x∃z∈B+𝑜xA⋅𝑜B+𝑜w⊆A⋅𝑜z→⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w⊆⋃z∈B+𝑜xA⋅𝑜z
219 217 218 syl ⊢Lim⁡x∧A∈On∧B∈On∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w⊆⋃z∈B+𝑜xA⋅𝑜z
220 219 adantrl ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w⊆⋃z∈B+𝑜xA⋅𝑜z
221 168 220 eqssd ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→⋃z∈B+𝑜xA⋅𝑜z=⋃w∈A⋅𝑜xA⋅𝑜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+𝑜xA⋅𝑜z
229 227 228 mpanr1 ⊢A∈On∧Lim⁡B+𝑜x→A⋅𝑜B+𝑜x=⋃z∈B+𝑜xA⋅𝑜z
230 226 229 syl ⊢Lim⁡x∧A∈On∧B∈On→A⋅𝑜B+𝑜x=⋃z∈B+𝑜xA⋅𝑜z
231 230 adantr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=⋃z∈B+𝑜xA⋅𝑜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⋅𝑜xA⋅𝑜B+𝑜w
241 232 239 240 syl2anc ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A→A⋅𝑜B+𝑜A⋅𝑜x=⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w
242 241 adantrr ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜A⋅𝑜x=⋃w∈A⋅𝑜xA⋅𝑜B+𝑜w
243 221 231 242 3eqtr4d ⊢Lim⁡x∧A∈On∧B∈On∧∅∈A∧∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=A⋅𝑜B+𝑜A⋅𝑜x
244 243 exp43 ⊢Lim⁡x→A∈On∧B∈On→∅∈A→∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=A⋅𝑜B+𝑜A⋅𝑜x
245 244 com3l ⊢A∈On∧B∈On→∅∈A→Lim⁡x→∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=A⋅𝑜B+𝑜A⋅𝑜x
246 245 imp ⊢A∈On∧B∈On∧∅∈A→Lim⁡x→∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=A⋅𝑜B+𝑜A⋅𝑜x
247 84 246 oe0lem ⊢A∈On∧B∈On→Lim⁡x→∀y∈xA⋅𝑜B+𝑜y=A⋅𝑜B+𝑜A⋅𝑜y→A⋅𝑜B+𝑜x=A⋅𝑜B+𝑜A⋅𝑜x
248 247 com12 ⊢Lim⁡x→A∈On∧B∈On→∀y∈xA⋅𝑜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