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