MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  odi Structured version   Visualization version   GIF version

Theorem odi 7893
Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.)
Assertion
Ref Expression
odi ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶)))

Proof of Theorem odi
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6879 . . . . . 6 (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 ∅))
21oveq2d 6887 . . . . 5 (𝑥 = ∅ → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 ∅)))
3 oveq2 6879 . . . . . 6 (𝑥 = ∅ → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 ∅))
43oveq2d 6887 . . . . 5 (𝑥 = ∅ → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 ∅)))
52, 4eqeq12d 2820 . . . 4 (𝑥 = ∅ → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) ↔ (𝐴 ·𝑜 (𝐵 +𝑜 ∅)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 ∅))))
6 oveq2 6879 . . . . . 6 (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦))
76oveq2d 6887 . . . . 5 (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)))
8 oveq2 6879 . . . . . 6 (𝑥 = 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝑦))
98oveq2d 6887 . . . . 5 (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))
107, 9eqeq12d 2820 . . . 4 (𝑥 = 𝑦 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) ↔ (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))))
11 oveq2 6879 . . . . . 6 (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦))
1211oveq2d 6887 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)))
13 oveq2 6879 . . . . . 6 (𝑥 = suc 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑦))
1413oveq2d 6887 . . . . 5 (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦)))
1512, 14eqeq12d 2820 . . . 4 (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) ↔ (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦))))
16 oveq2 6879 . . . . . 6 (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶))
1716oveq2d 6887 . . . . 5 (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)))
18 oveq2 6879 . . . . . 6 (𝑥 = 𝐶 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝐶))
1918oveq2d 6887 . . . . 5 (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶)))
2017, 19eqeq12d 2820 . . . 4 (𝑥 = 𝐶 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) ↔ (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶))))
21 omcl 7850 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On)
22 oa0 7830 . . . . . 6 ((𝐴 ·𝑜 𝐵) ∈ On → ((𝐴 ·𝑜 𝐵) +𝑜 ∅) = (𝐴 ·𝑜 𝐵))
2321, 22syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝐵) +𝑜 ∅) = (𝐴 ·𝑜 𝐵))
24 om0 7831 . . . . . . 7 (𝐴 ∈ On → (𝐴 ·𝑜 ∅) = ∅)
2524adantr 468 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 ∅) = ∅)
2625oveq2d 6887 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 ∅)) = ((𝐴 ·𝑜 𝐵) +𝑜 ∅))
27 oa0 7830 . . . . . . 7 (𝐵 ∈ On → (𝐵 +𝑜 ∅) = 𝐵)
2827adantl 469 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 ∅) = 𝐵)
2928oveq2d 6887 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 ∅)) = (𝐴 ·𝑜 𝐵))
3023, 26, 293eqtr4rd 2850 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 ∅)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 ∅)))
31 oveq1 6878 . . . . . . . 8 ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴))
32 oasuc 7838 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦))
33323adant1 1153 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦))
3433oveq2d 6887 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 ·𝑜 suc (𝐵 +𝑜 𝑦)))
35 oacl 7849 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On)
36 omsuc 7840 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 ·𝑜 suc (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴))
3735, 36sylan2 582 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·𝑜 suc (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴))
38373impb 1136 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 suc (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴))
3934, 38eqtrd 2839 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴))
40 omsuc 7840 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 suc 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝐴))
41403adant2 1154 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 suc 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝐴))
4241oveq2d 6887 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))
43 omcl 7850 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 𝑦) ∈ On)
44 oaass 7875 . . . . . . . . . . . . . . . . . 18 (((𝐴 ·𝑜 𝐵) ∈ On ∧ (𝐴 ·𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))
4521, 44syl3an1 1195 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ·𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))
4643, 45syl3an2 1196 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))
47463exp 1141 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))))
4847exp4b 419 . . . . . . . . . . . . . 14 (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))))))
4948pm2.43a 54 . . . . . . . . . . . . 13 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴))))))
5049com4r 94 . . . . . . . . . . . 12 (𝐴 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴))))))
5150pm2.43i 52 . . . . . . . . . . 11 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))))
52513imp 1130 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜 𝑦) +𝑜 𝐴)))
5342, 52eqtr4d 2842 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦)) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴))
5439, 53eqeq12d 2820 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦)) ↔ ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) +𝑜 𝐴)))
5531, 54syl5ibr 237 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦))))
56553exp 1141 . . . . . 6 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦))))))
5756com3r 87 . . . . 5 (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦))))))
5857impd 398 . . . 4 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 suc 𝑦)))))
59 vex 3393 . . . . . . . . . . . . . 14 𝑥 ∈ V
60 limelon 5998 . . . . . . . . . . . . . 14 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
6159, 60mpan 673 . . . . . . . . . . . . 13 (Lim 𝑥𝑥 ∈ On)
62 oacl 7849 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
63 om0r 7853 . . . . . . . . . . . . . . 15 ((𝐵 +𝑜 𝑥) ∈ On → (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ∅)
6462, 63syl 17 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ∅)
65 om0r 7853 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → (∅ ·𝑜 𝐵) = ∅)
66 om0r 7853 . . . . . . . . . . . . . . . 16 (𝑥 ∈ On → (∅ ·𝑜 𝑥) = ∅)
6765, 66oveqan12d 6890 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)) = (∅ +𝑜 ∅))
68 0elon 5988 . . . . . . . . . . . . . . . 16 ∅ ∈ On
69 oa0 7830 . . . . . . . . . . . . . . . 16 (∅ ∈ On → (∅ +𝑜 ∅) = ∅)
7068, 69ax-mp 5 . . . . . . . . . . . . . . 15 (∅ +𝑜 ∅) = ∅
7167, 70syl6req 2856 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ∅ = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)))
7264, 71eqtrd 2839 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)))
7361, 72sylan2 582 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ Lim 𝑥) → (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)))
7473ancoms 448 . . . . . . . . . . 11 ((Lim 𝑥𝐵 ∈ On) → (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)))
75 oveq1 6878 . . . . . . . . . . . 12 (𝐴 = ∅ → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (∅ ·𝑜 (𝐵 +𝑜 𝑥)))
76 oveq1 6878 . . . . . . . . . . . . 13 (𝐴 = ∅ → (𝐴 ·𝑜 𝐵) = (∅ ·𝑜 𝐵))
77 oveq1 6878 . . . . . . . . . . . . 13 (𝐴 = ∅ → (𝐴 ·𝑜 𝑥) = (∅ ·𝑜 𝑥))
7876, 77oveq12d 6889 . . . . . . . . . . . 12 (𝐴 = ∅ → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥)))
7975, 78eqeq12d 2820 . . . . . . . . . . 11 (𝐴 = ∅ → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) ↔ (∅ ·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜 𝐵) +𝑜 (∅ ·𝑜 𝑥))))
8074, 79syl5ibr 237 . . . . . . . . . 10 (𝐴 = ∅ → ((Lim 𝑥𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥))))
8180expd 402 . . . . . . . . 9 (𝐴 = ∅ → (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
8281com3r 87 . . . . . . . 8 (𝐵 ∈ On → (𝐴 = ∅ → (Lim 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
8382imp 395 . . . . . . 7 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥))))
8483a1dd 50 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
85 simplr 776 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝐵 ∈ On)
8662ancoms 448 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On)
87 onelon 5958 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵 +𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)
8886, 87sylan 571 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)
89 ontri1 5967 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ¬ 𝑧𝐵))
90 oawordex 7871 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧))
9189, 90bitr3d 272 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧𝐵 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧))
9285, 88, 91syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (¬ 𝑧𝐵 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧))
93 oaord 7861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 ↔ (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
94933expb 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣𝑥 ↔ (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
95 eleq1 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥)))
9694, 95sylan9bb 501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑣𝑥𝑧 ∈ (𝐵 +𝑜 𝑥)))
97 iba 519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣𝑥 ↔ (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
9897adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑣𝑥 ↔ (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
9996, 98bitr3d 272 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑧 ∈ (𝐵 +𝑜 𝑥) ↔ (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
10099an32s 634 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑣 ∈ On ∧ (𝐵 +𝑜 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +𝑜 𝑥) ↔ (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
101100biimpcd 240 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐵 +𝑜 𝑥) → (((𝑣 ∈ On ∧ (𝐵 +𝑜 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
102101exp4c 421 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))))
103102com4r 94 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))))
104103imp 395 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))))
105104reximdvai 3201 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧 → ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
10692, 105sylbid 231 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (¬ 𝑧𝐵 → ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
107106orrd 881 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
10861, 107sylanl1 662 . . . . . . . . . . . . . . . 16 (((Lim 𝑥𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
109108adantlrl 702 . . . . . . . . . . . . . . 15 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
110109adantlr 697 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))
111 0ellim 5997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Lim 𝑥 → ∅ ∈ 𝑥)
112 om00el 7890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜 𝑥) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥)))
113112biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥) → ∅ ∈ (𝐴 ·𝑜 𝑥)))
114111, 113sylan2i 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·𝑜 𝑥)))
11561, 114sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ Lim 𝑥) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·𝑜 𝑥)))
116115exp4b 419 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → (Lim 𝑥 → ∅ ∈ (𝐴 ·𝑜 𝑥)))))
117116com4r 94 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim 𝑥 → (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·𝑜 𝑥)))))
118117pm2.43a 54 . . . . . . . . . . . . . . . . . . . . . 22 (Lim 𝑥 → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·𝑜 𝑥))))
119118imp31 406 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ·𝑜 𝑥))
120119a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∅ ∈ (𝐴 ·𝑜 𝑥)))
121120adantlrr 703 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∅ ∈ (𝐴 ·𝑜 𝑥)))
122 omordi 7880 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵)))
123122ancom1s 635 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵)))
124 onelss 5976 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·𝑜 𝐵) ∈ On → ((𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 𝐵)))
12522sseq2d 3827 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·𝑜 𝐵) ∈ On → ((𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅) ↔ (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 𝐵)))
126124, 125sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ·𝑜 𝐵) ∈ On → ((𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
12721, 126syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
128127adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
129123, 128syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
130129adantll 696 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
131121, 130jcad 504 . . . . . . . . . . . . . . . . . 18 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (∅ ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅))))
132 oveq2 6879 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = ∅ → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) = ((𝐴 ·𝑜 𝐵) +𝑜 ∅))
133132sseq2d 3827 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ∅ → ((𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ↔ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)))
134133rspcev 3501 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 ∅)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
135131, 134syl6 35 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
136135adantrr 699 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → (𝑧𝐵 → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
137 omordi 7880 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣𝑥 → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥)))
13861, 137sylanl1 662 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣𝑥 → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥)))
139138adantrd 481 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥)))
140139adantrr 699 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥)))
141 oveq2 6879 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 → (𝐵 +𝑜 𝑦) = (𝐵 +𝑜 𝑣))
142141oveq2d 6887 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))
143 oveq2 6879 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 → (𝐴 ·𝑜 𝑦) = (𝐴 ·𝑜 𝑣))
144143oveq2d 6887 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))
145142, 144eqeq12d 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑣 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) ↔ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
146145rspccv 3498 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝑣𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
147 oveq2 6879 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = (𝐴 ·𝑜 𝑧))
148 eqeq1 2809 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = (𝐴 ·𝑜 𝑧) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) = (𝐴 ·𝑜 𝑧)))
149147, 148syl5ib 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) → ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) = (𝐴 ·𝑜 𝑧)))
150 eqimss2 3852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) = (𝐴 ·𝑜 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))
151149, 150syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)) → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
152151imim2i 16 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))) → (𝑣𝑥 → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))))
153152impd 398 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
154146, 153syl 17 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
155154ad2antll 711 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
156140, 155jcad 504 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ((𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))))
157 oveq2 6879 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))
158157sseq2d 3827 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ↔ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
159158rspcev 3501 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
160156, 159syl6 35 . . . . . . . . . . . . . . . . . 18 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
161160rexlimdvw 3221 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → (∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
162161adantlrr 703 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → (∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
163136, 162jaod 877 . . . . . . . . . . . . . . 15 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
164163adantr 468 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ((𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)))
165110, 164mpd 15 . . . . . . . . . . . . 13 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
166165ralrimiva 3153 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
167 iunss2 4753 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
168166, 167syl 17 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
169 omordlim 7891 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))
170169ex 399 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)))
17159, 170mpanr1 686 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ Lim 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)))
172171ancoms 448 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥𝐴 ∈ On) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)))
173172imp 395 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥𝐴 ∈ On) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))
174173adantlrr 703 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))
175174adantlr 697 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))
176 oaordi 7860 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
17761, 176sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥𝐵 ∈ On) → (𝑣𝑥 → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
178177imp 395 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥𝐵 ∈ On) ∧ 𝑣𝑥) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))
179178adantlrl 702 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))
180179a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
181180adantlr 697 . . . . . . . . . . . . . . . . . . 19 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)))
182 limord 5994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim 𝑥 → Ord 𝑥)
183 ordelon 5957 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord 𝑥𝑣𝑥) → 𝑣 ∈ On)
184182, 183sylan 571 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim 𝑥𝑣𝑥) → 𝑣 ∈ On)
185 omcl 7850 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑣 ∈ On) → (𝐴 ·𝑜 𝑣) ∈ On)
186185ancoms 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 𝑣) ∈ On)
187186adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 𝑣) ∈ On)
18821adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 𝐵) ∈ On)
189 oaordi 7860 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ·𝑜 𝑣) ∈ On ∧ (𝐴 ·𝑜 𝐵) ∈ On) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
190187, 188, 189syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
191184, 190sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim 𝑥𝑣𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
192191an32s 634 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
193192adantlr 697 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
194145rspccva 3500 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) ∧ 𝑣𝑥) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣)))
195194eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) ∧ 𝑣𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
196195adantll 696 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑣))))
197193, 196sylibrd 250 . . . . . . . . . . . . . . . . . . . 20 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
198 oacl 7849 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ On ∧ 𝑣 ∈ On) → (𝐵 +𝑜 𝑣) ∈ On)
199198ancoms 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑣) ∈ On)
200 omcl 7850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑣) ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On)
201199, 200sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On)
202201an12s 631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On)
203184, 202sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim 𝑥𝑣𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On)
204203an32s 634 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On)
205 onelss 5976 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
207206adantlr 697 . . . . . . . . . . . . . . . . . . . 20 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
208197, 207syld 47 . . . . . . . . . . . . . . . . . . 19 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
209181, 208jcad 504 . . . . . . . . . . . . . . . . . 18 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ∧ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))))
210 oveq2 6879 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐵 +𝑜 𝑣) → (𝐴 ·𝑜 𝑧) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))
211210sseq2d 3827 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐵 +𝑜 𝑣) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))
212211rspcev 3501 . . . . . . . . . . . . . . . . . 18 (((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ∧ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))
213209, 212syl6 35 . . . . . . . . . . . . . . . . 17 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)))
214213rexlimdva 3218 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) → (∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)))
215214adantr 468 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → (∃𝑣𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)))
216175, 215mpd 15 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))
217216ralrimiva 3153 . . . . . . . . . . . . 13 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) → ∀𝑤 ∈ (𝐴 ·𝑜 𝑥)∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))
218 iunss2 4753 . . . . . . . . . . . . 13 (∀𝑤 ∈ (𝐴 ·𝑜 𝑥)∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧) → 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
219217, 218syl 17 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦))) → 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
220219adantrl 698 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
221168, 220eqssd 3812 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) = 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
222 oalimcl 7874 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +𝑜 𝑥))
22359, 222mpanr1 686 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +𝑜 𝑥))
224223ancoms 448 . . . . . . . . . . . . . 14 ((Lim 𝑥𝐵 ∈ On) → Lim (𝐵 +𝑜 𝑥))
225224anim2i 605 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)))
226225an12s 631 . . . . . . . . . . . 12 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)))
227 ovex 6903 . . . . . . . . . . . . 13 (𝐵 +𝑜 𝑥) ∈ V
228 omlim 7847 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ ((𝐵 +𝑜 𝑥) ∈ V ∧ Lim (𝐵 +𝑜 𝑥))) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
229227, 228mpanr1 686 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
230226, 229syl 17 . . . . . . . . . . 11 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
231230adantr 468 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧))
23221ad2antlr 709 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝐴 ·𝑜 𝐵) ∈ On)
23359jctl 515 . . . . . . . . . . . . . . . . 17 (Lim 𝑥 → (𝑥 ∈ V ∧ Lim 𝑥))
234233anim2i 605 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ Lim 𝑥) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)))
235234ancoms 448 . . . . . . . . . . . . . . 15 ((Lim 𝑥𝐴 ∈ On) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)))
236 omlimcl 7892 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥))
237235, 236sylan 571 . . . . . . . . . . . . . 14 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥))
238237adantlrr 703 . . . . . . . . . . . . 13 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥))
239 ovex 6903 . . . . . . . . . . . . 13 (𝐴 ·𝑜 𝑥) ∈ V
240238, 239jctil 511 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝑥) ∈ V ∧ Lim (𝐴 ·𝑜 𝑥)))
241 oalim 7846 . . . . . . . . . . . 12 (((𝐴 ·𝑜 𝐵) ∈ On ∧ ((𝐴 ·𝑜 𝑥) ∈ V ∧ Lim (𝐴 ·𝑜 𝑥))) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
242232, 240, 241syl2anc 575 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
243242adantrr 699 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)) = 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤))
244221, 231, 2433eqtr4d 2849 . . . . . . . . 9 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)))) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))
245244exp43 425 . . . . . . . 8 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥))))))
246245com3l 89 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥))))))
247246imp 395 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
24884, 247oe0lem 7827 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
249248com12 32 . . . 4 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑦)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝑥)))))
2505, 10, 15, 20, 30, 58, 249tfinds3 7291 . . 3 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶))))
251250expdcom 401 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶)))))
2522513imp 1130 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2158  wral 3095  wrex 3096  Vcvv 3390  wss 3766  c0 4113   ciun 4708  Ord word 5932  Oncon0 5933  Lim wlim 5934  suc csuc 5935  (class class class)co 6871   +𝑜 coa 7790   ·𝑜 comu 7791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-oadd 7797  df-omul 7798
This theorem is referenced by:  omass  7894  oeeui  7916  oaabs2  7959
  Copyright terms: Public domain W3C validator