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 e. On /\ B e. On /\ C e. On ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )

Proof

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