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

Theorem odi 8617
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.)
Assertion
Ref Expression
odi ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))

Proof of Theorem odi
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7439 . . . . . 6 (𝑥 = ∅ → (𝐵 +o 𝑥) = (𝐵 +o ∅))
21oveq2d 7447 . . . . 5 (𝑥 = ∅ → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o ∅)))
3 oveq2 7439 . . . . . 6 (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o ∅))
43oveq2d 7447 . . . . 5 (𝑥 = ∅ → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o ∅)))
52, 4eqeq12d 2753 . . . 4 (𝑥 = ∅ → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o ∅)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o ∅))))
6 oveq2 7439 . . . . . 6 (𝑥 = 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o 𝑦))
76oveq2d 7447 . . . . 5 (𝑥 = 𝑦 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o 𝑦)))
8 oveq2 7439 . . . . . 6 (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦))
98oveq2d 7447 . . . . 5 (𝑥 = 𝑦 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))
107, 9eqeq12d 2753 . . . 4 (𝑥 = 𝑦 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))))
11 oveq2 7439 . . . . . 6 (𝑥 = suc 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o suc 𝑦))
1211oveq2d 7447 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o suc 𝑦)))
13 oveq2 7439 . . . . . 6 (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦))
1413oveq2d 7447 . . . . 5 (𝑥 = suc 𝑦 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))
1512, 14eqeq12d 2753 . . . 4 (𝑥 = suc 𝑦 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))))
16 oveq2 7439 . . . . . 6 (𝑥 = 𝐶 → (𝐵 +o 𝑥) = (𝐵 +o 𝐶))
1716oveq2d 7447 . . . . 5 (𝑥 = 𝐶 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o 𝐶)))
18 oveq2 7439 . . . . . 6 (𝑥 = 𝐶 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐶))
1918oveq2d 7447 . . . . 5 (𝑥 = 𝐶 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))
2017, 19eqeq12d 2753 . . . 4 (𝑥 = 𝐶 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))))
21 omcl 8574 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On)
22 oa0 8554 . . . . . 6 ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝐵) +o ∅) = (𝐴 ·o 𝐵))
2321, 22syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) +o ∅) = (𝐴 ·o 𝐵))
24 om0 8555 . . . . . . 7 (𝐴 ∈ On → (𝐴 ·o ∅) = ∅)
2524adantr 480 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o ∅) = ∅)
2625oveq2d 7447 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o ∅)) = ((𝐴 ·o 𝐵) +o ∅))
27 oa0 8554 . . . . . . 7 (𝐵 ∈ On → (𝐵 +o ∅) = 𝐵)
2827adantl 481 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o ∅) = 𝐵)
2928oveq2d 7447 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o ∅)) = (𝐴 ·o 𝐵))
3023, 26, 293eqtr4rd 2788 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o ∅)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o ∅)))
31 oveq1 7438 . . . . . . . 8 ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴))
32 oasuc 8562 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦))
33323adant1 1131 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦))
3433oveq2d 7447 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o (𝐵 +o suc 𝑦)) = (𝐴 ·o suc (𝐵 +o 𝑦)))
35 oacl 8573 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o 𝑦) ∈ On)
36 omsuc 8564 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐵 +o 𝑦) ∈ On) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴))
3735, 36sylan2 593 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴))
38373impb 1115 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴))
3934, 38eqtrd 2777 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴))
40 omsuc 8564 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴))
41403adant2 1132 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴))
4241oveq2d 7447 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))
43 omcl 8574 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑦) ∈ On)
44 oaass 8599 . . . . . . . . . . . . . . . . . 18 (((𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))
4521, 44syl3an1 1164 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))
4643, 45syl3an2 1165 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))
47463exp 1120 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))))
4847exp4b 430 . . . . . . . . . . . . . 14 (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))))))
4948pm2.43a 54 . . . . . . . . . . . . 13 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))))))
5049com4r 94 . . . . . . . . . . . 12 (𝐴 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))))))
5150pm2.43i 52 . . . . . . . . . . 11 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))))
52513imp 1111 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))
5342, 52eqtr4d 2780 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴))
5439, 53eqeq12d 2753 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) ↔ ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴)))
5531, 54imbitrrid 246 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))))
56553exp 1120 . . . . . 6 (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))))))
5756com3r 87 . . . . 5 (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))))))
5857impd 410 . . . 4 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))))
59 vex 3484 . . . . . . . . . . . . . 14 𝑥 ∈ V
60 limelon 6448 . . . . . . . . . . . . . 14 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
6159, 60mpan 690 . . . . . . . . . . . . 13 (Lim 𝑥𝑥 ∈ On)
62 oacl 8573 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +o 𝑥) ∈ On)
63 om0r 8577 . . . . . . . . . . . . . . 15 ((𝐵 +o 𝑥) ∈ On → (∅ ·o (𝐵 +o 𝑥)) = ∅)
6462, 63syl 17 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅ ·o (𝐵 +o 𝑥)) = ∅)
65 om0r 8577 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → (∅ ·o 𝐵) = ∅)
66 om0r 8577 . . . . . . . . . . . . . . . 16 (𝑥 ∈ On → (∅ ·o 𝑥) = ∅)
6765, 66oveqan12d 7450 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((∅ ·o 𝐵) +o (∅ ·o 𝑥)) = (∅ +o ∅))
68 0elon 6438 . . . . . . . . . . . . . . . 16 ∅ ∈ On
69 oa0 8554 . . . . . . . . . . . . . . . 16 (∅ ∈ On → (∅ +o ∅) = ∅)
7068, 69ax-mp 5 . . . . . . . . . . . . . . 15 (∅ +o ∅) = ∅
7167, 70eqtr2di 2794 . . . . . . . . . . . . . 14 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ∅ = ((∅ ·o 𝐵) +o (∅ ·o 𝑥)))
7264, 71eqtrd 2777 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅ ·o (𝐵 +o 𝑥)) = ((∅ ·o 𝐵) +o (∅ ·o 𝑥)))
7361, 72sylan2 593 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ Lim 𝑥) → (∅ ·o (𝐵 +o 𝑥)) = ((∅ ·o 𝐵) +o (∅ ·o 𝑥)))
7473ancoms 458 . . . . . . . . . . 11 ((Lim 𝑥𝐵 ∈ On) → (∅ ·o (𝐵 +o 𝑥)) = ((∅ ·o 𝐵) +o (∅ ·o 𝑥)))
75 oveq1 7438 . . . . . . . . . . . 12 (𝐴 = ∅ → (𝐴 ·o (𝐵 +o 𝑥)) = (∅ ·o (𝐵 +o 𝑥)))
76 oveq1 7438 . . . . . . . . . . . . 13 (𝐴 = ∅ → (𝐴 ·o 𝐵) = (∅ ·o 𝐵))
77 oveq1 7438 . . . . . . . . . . . . 13 (𝐴 = ∅ → (𝐴 ·o 𝑥) = (∅ ·o 𝑥))
7876, 77oveq12d 7449 . . . . . . . . . . . 12 (𝐴 = ∅ → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((∅ ·o 𝐵) +o (∅ ·o 𝑥)))
7975, 78eqeq12d 2753 . . . . . . . . . . 11 (𝐴 = ∅ → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (∅ ·o (𝐵 +o 𝑥)) = ((∅ ·o 𝐵) +o (∅ ·o 𝑥))))
8074, 79imbitrrid 246 . . . . . . . . . 10 (𝐴 = ∅ → ((Lim 𝑥𝐵 ∈ On) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))
8180expd 415 . . . . . . . . 9 (𝐴 = ∅ → (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
8281com3r 87 . . . . . . . 8 (𝐵 ∈ On → (𝐴 = ∅ → (Lim 𝑥 → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
8382imp 406 . . . . . . 7 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))
8483a1dd 50 . . . . . 6 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
85 simplr 769 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝐵 ∈ On)
8662ancoms 458 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑥) ∈ On)
87 onelon 6409 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵 +o 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On)
8886, 87sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On)
89 ontri1 6418 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ¬ 𝑧𝐵))
90 oawordex 8595 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵𝑧 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧))
9189, 90bitr3d 281 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧𝐵 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧))
9285, 88, 91syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (¬ 𝑧𝐵 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧))
93 oaord 8585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 ↔ (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
94933expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣𝑥 ↔ (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
95 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 +o 𝑣) = 𝑧 → ((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ↔ 𝑧 ∈ (𝐵 +o 𝑥)))
9694, 95sylan9bb 509 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑣𝑥𝑧 ∈ (𝐵 +o 𝑥)))
97 iba 527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 +o 𝑣) = 𝑧 → (𝑣𝑥 ↔ (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
9897adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑣𝑥 ↔ (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
9996, 98bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑧 ∈ (𝐵 +o 𝑥) ↔ (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
10099an32s 652 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑣 ∈ On ∧ (𝐵 +o 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +o 𝑥) ↔ (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
101100biimpcd 249 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐵 +o 𝑥) → (((𝑣 ∈ On ∧ (𝐵 +o 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
102101exp4c 432 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐵 +o 𝑥) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))))
103102com4r 94 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))))
104103imp 406 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))))
105104reximdvai 3165 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧 → ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
10692, 105sylbid 240 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (¬ 𝑧𝐵 → ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
107106orrd 864 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
10861, 107sylanl1 680 . . . . . . . . . . . . . . . 16 (((Lim 𝑥𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
109108adantlrl 720 . . . . . . . . . . . . . . 15 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
110109adantlr 715 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))
111 0ellim 6447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Lim 𝑥 → ∅ ∈ 𝑥)
112 om00el 8614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·o 𝑥) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥)))
113112biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥) → ∅ ∈ (𝐴 ·o 𝑥)))
114111, 113sylan2i 606 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·o 𝑥)))
11561, 114sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ Lim 𝑥) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·o 𝑥)))
116115exp4b 430 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → (Lim 𝑥 → ∅ ∈ (𝐴 ·o 𝑥)))))
117116com4r 94 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim 𝑥 → (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·o 𝑥)))))
118117pm2.43a 54 . . . . . . . . . . . . . . . . . . . . . 22 (Lim 𝑥 → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·o 𝑥))))
119118imp31 417 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ·o 𝑥))
120119a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∅ ∈ (𝐴 ·o 𝑥)))
121120adantlrr 721 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∅ ∈ (𝐴 ·o 𝑥)))
122 omordi 8604 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵)))
123122ancom1s 653 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵)))
124 onelss 6426 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ (𝐴 ·o 𝐵)))
12522sseq2d 4016 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅) ↔ (𝐴 ·o 𝑧) ⊆ (𝐴 ·o 𝐵)))
126124, 125sylibrd 259 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
12721, 126syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
128127adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
129123, 128syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
130129adantll 714 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
131121, 130jcad 512 . . . . . . . . . . . . . . . . . 18 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → (∅ ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))))
132 oveq2 7439 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = ∅ → ((𝐴 ·o 𝐵) +o 𝑤) = ((𝐴 ·o 𝐵) +o ∅))
133132sseq2d 4016 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ∅ → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) ↔ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))
134133rspcev 3622 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))
135131, 134syl6 35 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧𝐵 → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
136135adantrr 717 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝑧𝐵 → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
137 omordi 8604 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣𝑥 → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥)))
13861, 137sylanl1 680 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣𝑥 → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥)))
139138adantrd 491 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥)))
140139adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥)))
141 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 → (𝐵 +o 𝑦) = (𝐵 +o 𝑣))
142141oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → (𝐴 ·o (𝐵 +o 𝑦)) = (𝐴 ·o (𝐵 +o 𝑣)))
143 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 → (𝐴 ·o 𝑦) = (𝐴 ·o 𝑣))
144143oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))
145142, 144eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑣 → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ↔ (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
146145rspccv 3619 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝑣𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
147 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o (𝐵 +o 𝑣)) = (𝐴 ·o 𝑧))
148 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐴 ·o (𝐵 +o 𝑣)) = (𝐴 ·o 𝑧) ↔ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧)))
149147, 148imbitrid 244 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐵 +o 𝑣) = 𝑧 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧)))
150 eqimss2 4043 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))
151149, 150syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
152151imim2i 16 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → (𝑣𝑥 → ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))))
153152impd 410 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
154146, 153syl 17 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
155154ad2antll 729 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
156140, 155jcad 512 . . . . . . . . . . . . . . . . . . 19 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ((𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))))
157 oveq2 7439 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))
158157sseq2d 4016 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐴 ·o 𝑣) → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) ↔ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
159158rspcev 3622 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))
160156, 159syl6 35 . . . . . . . . . . . . . . . . . 18 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
161160rexlimdvw 3160 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
162161adantlrr 721 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
163136, 162jaod 860 . . . . . . . . . . . . . . 15 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
164163adantr 480 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ((𝑧𝐵 ∨ ∃𝑣 ∈ On (𝑣𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)))
165110, 164mpd 15 . . . . . . . . . . . . 13 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))
166165ralrimiva 3146 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))
167 iunss2 5049 . . . . . . . . . . . 12 (∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) ⊆ 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
168166, 167syl 17 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) ⊆ 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
169 omordlim 8615 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣))
170169ex 412 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣)))
17159, 170mpanr1 703 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ Lim 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣)))
172171ancoms 458 . . . . . . . . . . . . . . . . . 18 ((Lim 𝑥𝐴 ∈ On) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣)))
173172imp 406 . . . . . . . . . . . . . . . . 17 (((Lim 𝑥𝐴 ∈ On) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣))
174173adantlrr 721 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣))
175174adantlr 715 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣))
176 oaordi 8584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣𝑥 → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
17761, 176sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim 𝑥𝐵 ∈ On) → (𝑣𝑥 → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
178177imp 406 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥𝐵 ∈ On) ∧ 𝑣𝑥) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))
179178adantlrl 720 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))
180179a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
181180adantlr 715 . . . . . . . . . . . . . . . . . . 19 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)))
182 limord 6444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim 𝑥 → Ord 𝑥)
183 ordelon 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord 𝑥𝑣𝑥) → 𝑣 ∈ On)
184182, 183sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim 𝑥𝑣𝑥) → 𝑣 ∈ On)
185 omcl 8574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑣 ∈ On) → (𝐴 ·o 𝑣) ∈ On)
186185ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·o 𝑣) ∈ On)
187186adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o 𝑣) ∈ On)
18821adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o 𝐵) ∈ On)
189 oaordi 8584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ·o 𝑣) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
190187, 188, 189syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
191184, 190sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim 𝑥𝑣𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
192191an32s 652 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
193192adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
194145rspccva 3621 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ∧ 𝑣𝑥) → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))
195194eleq2d 2827 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ∧ 𝑣𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
196195adantll 714 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))
197193, 196sylibrd 259 . . . . . . . . . . . . . . . . . . . 20 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣))))
198 oacl 8573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ On ∧ 𝑣 ∈ On) → (𝐵 +o 𝑣) ∈ On)
199198ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑣) ∈ On)
200 omcl 8574 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ (𝐵 +o 𝑣) ∈ On) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On)
201199, 200sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On)
202201an12s 649 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On)
203184, 202sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim 𝑥𝑣𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On)
204203an32s 652 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On)
205 onelss 6426 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ·o (𝐵 +o 𝑣)) ∈ On → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))
207206adantlr 715 . . . . . . . . . . . . . . . . . . . 20 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))
208197, 207syld 47 . . . . . . . . . . . . . . . . . . 19 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))
209181, 208jcad 512 . . . . . . . . . . . . . . . . . 18 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ∧ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))))
210 oveq2 7439 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐵 +o 𝑣) → (𝐴 ·o 𝑧) = (𝐴 ·o (𝐵 +o 𝑣)))
211210sseq2d 4016 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐵 +o 𝑣) → (((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))
212211rspcev 3622 . . . . . . . . . . . . . . . . . 18 (((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ∧ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))
213209, 212syl6 35 . . . . . . . . . . . . . . . . 17 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)))
214213rexlimdva 3155 . . . . . . . . . . . . . . . 16 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → (∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)))
215214adantr 480 . . . . . . . . . . . . . . 15 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → (∃𝑣𝑥 𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)))
216175, 215mpd 15 . . . . . . . . . . . . . 14 ((((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))
217216ralrimiva 3146 . . . . . . . . . . . . 13 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → ∀𝑤 ∈ (𝐴 ·o 𝑥)∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))
218 iunss2 5049 . . . . . . . . . . . . 13 (∀𝑤 ∈ (𝐴 ·o 𝑥)∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧) → 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
219217, 218syl 17 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
220219adantrl 716 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
221168, 220eqssd 4001 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) = 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
222 oalimcl 8598 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +o 𝑥))
22359, 222mpanr1 703 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +o 𝑥))
224223ancoms 458 . . . . . . . . . . . . . 14 ((Lim 𝑥𝐵 ∈ On) → Lim (𝐵 +o 𝑥))
225224anim2i 617 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (Lim 𝑥𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)))
226225an12s 649 . . . . . . . . . . . 12 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)))
227 ovex 7464 . . . . . . . . . . . . 13 (𝐵 +o 𝑥) ∈ V
228 omlim 8571 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ ((𝐵 +o 𝑥) ∈ V ∧ Lim (𝐵 +o 𝑥))) → (𝐴 ·o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
229227, 228mpanr1 703 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)) → (𝐴 ·o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
230226, 229syl 17 . . . . . . . . . . 11 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
231230adantr 480 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝐴 ·o (𝐵 +o 𝑥)) = 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧))
23221ad2antlr 727 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) ∈ On)
23359jctl 523 . . . . . . . . . . . . . . . 16 (Lim 𝑥 → (𝑥 ∈ V ∧ Lim 𝑥))
234233anim1ci 616 . . . . . . . . . . . . . . 15 ((Lim 𝑥𝐴 ∈ On) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)))
235 omlimcl 8616 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥))
236234, 235sylan 580 . . . . . . . . . . . . . 14 (((Lim 𝑥𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥))
237236adantlrr 721 . . . . . . . . . . . . 13 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥))
238 ovex 7464 . . . . . . . . . . . . 13 (𝐴 ·o 𝑥) ∈ V
239237, 238jctil 519 . . . . . . . . . . . 12 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝑥) ∈ V ∧ Lim (𝐴 ·o 𝑥)))
240 oalim 8570 . . . . . . . . . . . 12 (((𝐴 ·o 𝐵) ∈ On ∧ ((𝐴 ·o 𝑥) ∈ V ∧ Lim (𝐴 ·o 𝑥))) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
241232, 239, 240syl2anc 584 . . . . . . . . . . 11 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
242241adantrr 717 . . . . . . . . . 10 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤))
243221, 231, 2423eqtr4d 2787 . . . . . . . . 9 (((Lim 𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))
244243exp43 436 . . . . . . . 8 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))))
245244com3l 89 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))))
246245imp 406 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
24784, 246oe0lem 8551 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝑥 → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
248247com12 32 . . . 4 (Lim 𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∀𝑦𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))
2495, 10, 15, 20, 30, 58, 248tfinds3 7886 . . 3 (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))))
250249expdcom 414 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))))
2512503imp 1111 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  wss 3951  c0 4333   ciun 4991  Ord word 6383  Oncon0 6384  Lim wlim 6385  suc csuc 6386  (class class class)co 7431   +o coa 8503   ·o comu 8504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-omul 8511
This theorem is referenced by:  omass  8618  oeeui  8640  oaabs2  8687  oaabsb  43307  naddwordnexlem4  43414
  Copyright terms: Public domain W3C validator