MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  odi Structured version   Visualization version   GIF version
Theorem odi 8579
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 7417 . . . . . 6 (π‘₯ = βˆ… β†’ (𝐡 +o π‘₯) = (𝐡 +o βˆ…))
21oveq2d 7425 . . . . 5 (π‘₯ = βˆ… β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o βˆ…)))
3 oveq2 7417 . . . . . 6 (π‘₯ = βˆ… β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o βˆ…))
43oveq2d 7425 . . . . 5 (π‘₯ = βˆ… β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)))
52, 4eqeq12d 2749 . . . 4 (π‘₯ = βˆ… β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o βˆ…)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…))))
6 oveq2 7417 . . . . . 6 (π‘₯ = 𝑦 β†’ (𝐡 +o π‘₯) = (𝐡 +o 𝑦))
76oveq2d 7425 . . . . 5 (π‘₯ = 𝑦 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o 𝑦)))
8 oveq2 7417 . . . . . 6 (π‘₯ = 𝑦 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o 𝑦))
98oveq2d 7425 . . . . 5 (π‘₯ = 𝑦 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))
107, 9eqeq12d 2749 . . . 4 (π‘₯ = 𝑦 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))))
11 oveq2 7417 . . . . . 6 (π‘₯ = suc 𝑦 β†’ (𝐡 +o π‘₯) = (𝐡 +o suc 𝑦))
1211oveq2d 7425 . . . . 5 (π‘₯ = suc 𝑦 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o suc 𝑦)))
13 oveq2 7417 . . . . . 6 (π‘₯ = suc 𝑦 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o suc 𝑦))
1413oveq2d 7425 . . . . 5 (π‘₯ = suc 𝑦 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)))
1512, 14eqeq12d 2749 . . . 4 (π‘₯ = suc 𝑦 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦))))
16 oveq2 7417 . . . . . 6 (π‘₯ = 𝐢 β†’ (𝐡 +o π‘₯) = (𝐡 +o 𝐢))
1716oveq2d 7425 . . . . 5 (π‘₯ = 𝐢 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o 𝐢)))
18 oveq2 7417 . . . . . 6 (π‘₯ = 𝐢 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o 𝐢))
1918oveq2d 7425 . . . . 5 (π‘₯ = 𝐢 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))
2017, 19eqeq12d 2749 . . . 4 (π‘₯ = 𝐢 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢))))
21 omcl 8536 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o 𝐡) ∈ On)
22 oa0 8516 . . . . . 6 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝐡) +o βˆ…) = (𝐴 Β·o 𝐡))
2321, 22syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o βˆ…) = (𝐴 Β·o 𝐡))
24 om0 8517 . . . . . . 7 (𝐴 ∈ On β†’ (𝐴 Β·o βˆ…) = βˆ…)
2524adantr 482 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o βˆ…) = βˆ…)
2625oveq2d 7425 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)) = ((𝐴 Β·o 𝐡) +o βˆ…))
27 oa0 8516 . . . . . . 7 (𝐡 ∈ On β†’ (𝐡 +o βˆ…) = 𝐡)
2827adantl 483 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o βˆ…) = 𝐡)
2928oveq2d 7425 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o βˆ…)) = (𝐴 Β·o 𝐡))
3023, 26, 293eqtr4rd 2784 . . . 4 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o βˆ…)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)))
31 oveq1 7416 . . . . . . . 8 ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴) = (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴))
32 oasuc 8524 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o suc 𝑦) = suc (𝐡 +o 𝑦))
33323adant1 1131 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o suc 𝑦) = suc (𝐡 +o 𝑦))
3433oveq2d 7425 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = (𝐴 Β·o suc (𝐡 +o 𝑦)))
35 oacl 8535 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o 𝑦) ∈ On)
36 omsuc 8526 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐡 +o 𝑦) ∈ On) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
3735, 36sylan2 594 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝐡 ∈ On ∧ 𝑦 ∈ On)) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
38373impb 1116 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
3934, 38eqtrd 2773 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
40 omsuc 8526 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc 𝑦) = ((𝐴 Β·o 𝑦) +o 𝐴))
41403adant2 1132 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc 𝑦) = ((𝐴 Β·o 𝑦) +o 𝐴))
4241oveq2d 7425 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
43 omcl 8536 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o 𝑦) ∈ On)
44 oaass 8561 . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . 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 1112 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
5342, 52eqtr4d 2776 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)) = (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴))
5439, 53eqeq12d 2749 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ ((𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)) ↔ ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴) = (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴)))
5531, 54imbitrrid 245 . . . . . . 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 412 . . . 4 (𝑦 ∈ On β†’ ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)))))
59 vex 3479 . . . . . . . . . . . . . 14 π‘₯ ∈ V
60 limelon 6429 . . . . . . . . . . . . . 14 ((π‘₯ ∈ V ∧ Lim π‘₯) β†’ π‘₯ ∈ On)
6159, 60mpan 689 . . . . . . . . . . . . 13 (Lim π‘₯ β†’ π‘₯ ∈ On)
62 oacl 8535 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (𝐡 +o π‘₯) ∈ On)
63 om0r 8539 . . . . . . . . . . . . . . 15 ((𝐡 +o π‘₯) ∈ On β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = βˆ…)
6462, 63syl 17 . . . . . . . . . . . . . 14 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = βˆ…)
65 om0r 8539 . . . . . . . . . . . . . . . 16 (𝐡 ∈ On β†’ (βˆ… Β·o 𝐡) = βˆ…)
66 om0r 8539 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ On β†’ (βˆ… Β·o π‘₯) = βˆ…)
6765, 66oveqan12d 7428 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)) = (βˆ… +o βˆ…))
68 0elon 6419 . . . . . . . . . . . . . . . 16 βˆ… ∈ On
69 oa0 8516 . . . . . . . . . . . . . . . 16 (βˆ… ∈ On β†’ (βˆ… +o βˆ…) = βˆ…)
7068, 69ax-mp 5 . . . . . . . . . . . . . . 15 (βˆ… +o βˆ…) = βˆ…
7167, 70eqtr2di 2790 . . . . . . . . . . . . . 14 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ βˆ… = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7264, 71eqtrd 2773 . . . . . . . . . . . . 13 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7361, 72sylan2 594 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ Lim π‘₯) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7473ancoms 460 . . . . . . . . . . 11 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
75 oveq1 7416 . . . . . . . . . . . 12 (𝐴 = βˆ… β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (βˆ… Β·o (𝐡 +o π‘₯)))
76 oveq1 7416 . . . . . . . . . . . . 13 (𝐴 = βˆ… β†’ (𝐴 Β·o 𝐡) = (βˆ… Β·o 𝐡))
77 oveq1 7416 . . . . . . . . . . . . 13 (𝐴 = βˆ… β†’ (𝐴 Β·o π‘₯) = (βˆ… Β·o π‘₯))
7876, 77oveq12d 7427 . . . . . . . . . . . 12 (𝐴 = βˆ… β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7975, 78eqeq12d 2749 . . . . . . . . . . 11 (𝐴 = βˆ… β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯))))
8074, 79imbitrrid 245 . . . . . . . . . 10 (𝐴 = βˆ… β†’ ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯))))
8180expd 417 . . . . . . . . 9 (𝐴 = βˆ… β†’ (Lim π‘₯ β†’ (𝐡 ∈ On β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
8281com3r 87 . . . . . . . 8 (𝐡 ∈ On β†’ (𝐴 = βˆ… β†’ (Lim π‘₯ β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
8382imp 408 . . . . . . 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 768 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝐡 ∈ On)
8662ancoms 460 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o π‘₯) ∈ On)
87 onelon 6390 . . . . . . . . . . . . . . . . . . . . 21 (((𝐡 +o π‘₯) ∈ On ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝑧 ∈ On)
8886, 87sylan 581 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝑧 ∈ On)
89 ontri1 6399 . . . . . . . . . . . . . . . . . . . . 21 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (𝐡 βŠ† 𝑧 ↔ Β¬ 𝑧 ∈ 𝐡))
90 oawordex 8557 . . . . . . . . . . . . . . . . . . . . 21 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (𝐡 βŠ† 𝑧 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
9189, 90bitr3d 281 . . . . . . . . . . . . . . . . . . . 20 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (Β¬ 𝑧 ∈ 𝐡 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
9285, 88, 91syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (Β¬ 𝑧 ∈ 𝐡 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
93 oaord 8547 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ On ∧ π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ ↔ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
94933expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑣 ∈ π‘₯ ↔ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
95 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 +o 𝑣) = 𝑧 β†’ ((𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯) ↔ 𝑧 ∈ (𝐡 +o π‘₯)))
9694, 95sylan9bb 511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑣 ∈ π‘₯ ↔ 𝑧 ∈ (𝐡 +o π‘₯)))
97 iba 529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
9897adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑣 ∈ π‘₯ ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
9996, 98bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑧 ∈ (𝐡 +o π‘₯) ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10099an32s 651 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑣 ∈ On ∧ (𝐡 +o 𝑣) = 𝑧) ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑧 ∈ (𝐡 +o π‘₯) ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
101100biimpcd 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐡 +o π‘₯) β†’ (((𝑣 ∈ On ∧ (𝐡 +o 𝑣) = 𝑧) ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
102101exp4c 434 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐡 +o π‘₯) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))))
103102com4r 94 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑧 ∈ (𝐡 +o π‘₯) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))))
104103imp 408 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧))))
105104reximdvai 3166 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧 β†’ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10692, 105sylbid 239 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (Β¬ 𝑧 ∈ 𝐡 β†’ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
107106orrd 862 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10861, 107sylanl1 679 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
109108adantlrl 719 . . . . . . . . . . . . . . 15 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
110109adantlr 714 . . . . . . . . . . . . . 14 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
111 0ellim 6428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Lim π‘₯ β†’ βˆ… ∈ π‘₯)
112 om00el 8576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… ∈ (𝐴 Β·o π‘₯) ↔ (βˆ… ∈ 𝐴 ∧ βˆ… ∈ π‘₯)))
113112biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… ∈ 𝐴 ∧ βˆ… ∈ π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
114111, 113sylan2i 607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… ∈ 𝐴 ∧ Lim π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
11561, 114sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ Lim π‘₯) β†’ ((βˆ… ∈ 𝐴 ∧ Lim π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
116115exp4b 432 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On β†’ (Lim π‘₯ β†’ (βˆ… ∈ 𝐴 β†’ (Lim π‘₯ β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))))
117116com4r 94 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim π‘₯ β†’ (𝐴 ∈ On β†’ (Lim π‘₯ β†’ (βˆ… ∈ 𝐴 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))))
118117pm2.43a 54 . . . . . . . . . . . . . . . . . . . . . 22 (Lim π‘₯ β†’ (𝐴 ∈ On β†’ (βˆ… ∈ 𝐴 β†’ βˆ… ∈ (𝐴 Β·o π‘₯))))
119118imp31 419 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ βˆ… ∈ (𝐴 Β·o π‘₯))
120119a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
121120adantlrr 720 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
122 omordi 8566 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐡 ∈ On ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡)))
123122ancom1s 652 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡)))
124 onelss 6407 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† (𝐴 Β·o 𝐡)))
12522sseq2d 4015 . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
129123, 128syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
130129adantll 713 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
131121, 130jcad 514 . . . . . . . . . . . . . . . . . 18 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (βˆ… ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…))))
132 oveq2 7417 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = βˆ… β†’ ((𝐴 Β·o 𝐡) +o 𝑀) = ((𝐴 Β·o 𝐡) +o βˆ…))
133132sseq2d 4015 . . . . . . . . . . . . . . . . . . 19 (𝑀 = βˆ… β†’ ((𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀) ↔ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
134133rspcev 3613 . . . . . . . . . . . . . . . . . 18 ((βˆ… ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀))
135131, 134syl6 35 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
136135adantrr 716 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝑧 ∈ 𝐡 β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
137 omordi 8566 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘₯ ∈ On ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
13861, 137sylanl1 679 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
139138adantrd 493 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
140139adantrr 716 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
141 oveq2 7417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 β†’ (𝐡 +o 𝑦) = (𝐡 +o 𝑣))
142141oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 β†’ (𝐴 Β·o (𝐡 +o 𝑦)) = (𝐴 Β·o (𝐡 +o 𝑣)))
143 oveq2 7417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 β†’ (𝐴 Β·o 𝑦) = (𝐴 Β·o 𝑣))
144143oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
145142, 144eqeq12d 2749 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑣 β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ↔ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
146145rspccv 3610 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
147 oveq2 7417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐡 +o 𝑣) = 𝑧 β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = (𝐴 Β·o 𝑧))
148 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)) β†’ ((𝐴 Β·o (𝐡 +o 𝑣)) = (𝐴 Β·o 𝑧) ↔ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)) = (𝐴 Β·o 𝑧)))
149147, 148imbitrid 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)) β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)) = (𝐴 Β·o 𝑧)))
150 eqimss2 4042 . . . . . . . . . . . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
156140, 155jcad 514 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ ((𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))))
157 oveq2 7417 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
158157sseq2d 4015 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀) ↔ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
159158rspcev 3613 . . . . . . . . . . . . . . . . . . 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 3161 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
162161adantlrr 720 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
163136, 162jaod 858 . . . . . . . . . . . . . . 15 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
164163adantr 482 . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆ€π‘§ ∈ (𝐡 +o π‘₯)βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀))
167 iunss2 5053 . . . . . . . . . . . 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 8577 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
170169ex 414 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
17159, 170mpanr1 702 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ Lim π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
172171ancoms 460 . . . . . . . . . . . . . . . . . 18 ((Lim π‘₯ ∧ 𝐴 ∈ On) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
173172imp 408 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
174173adantlrr 720 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
175174adantlr 714 . . . . . . . . . . . . . . 15 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
176 oaordi 8546 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
17761, 176sylan 581 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
178177imp 408 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ 𝐡 ∈ On) ∧ 𝑣 ∈ π‘₯) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯))
179178adantlrl 719 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯))
180179a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
181180adantlr 714 . . . . . . . . . . . . . . . . . . 19 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
182 limord 6425 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim π‘₯ β†’ Ord π‘₯)
183 ordelon 6389 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord π‘₯ ∧ 𝑣 ∈ π‘₯) β†’ 𝑣 ∈ On)
184182, 183sylan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) β†’ 𝑣 ∈ On)
185 omcl 8536 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑣 ∈ On) β†’ (𝐴 Β·o 𝑣) ∈ On)
186185ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐴 ∈ On) β†’ (𝐴 Β·o 𝑣) ∈ On)
187186adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o 𝑣) ∈ On)
18821adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o 𝐡) ∈ On)
189 oaordi 8546 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 Β·o 𝑣) ∈ On ∧ (𝐴 Β·o 𝐡) ∈ On) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
190187, 188, 189syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
191184, 190sylan 581 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
192191an32s 651 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
193192adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
194145rspccva 3612 . . . . . . . . . . . . . . . . . . . . . . 23 ((βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
195194eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . 22 ((βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ∧ 𝑣 ∈ π‘₯) β†’ (((𝐴 Β·o 𝐡) +o 𝑀) ∈ (𝐴 Β·o (𝐡 +o 𝑣)) ↔ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
196195adantll 713 . . . . . . . . . . . . . . . . . . . . 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 8535 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 ∈ On ∧ 𝑣 ∈ On) β†’ (𝐡 +o 𝑣) ∈ On)
199198ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o 𝑣) ∈ On)
200 omcl 8536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ (𝐡 +o 𝑣) ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
201199, 200sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
202201an12s 648 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
203184, 202sylan 581 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
204203an32s 651 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
205 onelss 6407 . . . . . . . . . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . . . . . . . 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 514 . . . . . . . . . . . . . . . . . 18 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯) ∧ ((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o (𝐡 +o 𝑣)))))
210 oveq2 7417 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐡 +o 𝑣) β†’ (𝐴 Β·o 𝑧) = (𝐴 Β·o (𝐡 +o 𝑣)))
211210sseq2d 4015 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐡 +o 𝑣) β†’ (((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧) ↔ ((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o (𝐡 +o 𝑣))))
212211rspcev 3613 . . . . . . . . . . . . . . . . . 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 3156 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) β†’ (βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣) β†’ βˆƒπ‘§ ∈ (𝐡 +o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧)))
215214adantr 482 . . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . . 13 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) β†’ βˆ€π‘€ ∈ (𝐴 Β·o π‘₯)βˆƒπ‘§ ∈ (𝐡 +o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧))
218 iunss2 5053 . . . . . . . . . . . . 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 715 . . . . . . . . . . 11 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
221168, 220eqssd 4000 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
222 oalimcl 8560 . . . . . . . . . . . . . . . 16 ((𝐡 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) β†’ Lim (𝐡 +o π‘₯))
22359, 222mpanr1 702 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ Lim π‘₯) β†’ Lim (𝐡 +o π‘₯))
224223ancoms 460 . . . . . . . . . . . . . 14 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ Lim (𝐡 +o π‘₯))
225224anim2i 618 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (Lim π‘₯ ∧ 𝐡 ∈ On)) β†’ (𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)))
226225an12s 648 . . . . . . . . . . . 12 ((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)))
227 ovex 7442 . . . . . . . . . . . . 13 (𝐡 +o π‘₯) ∈ V
228 omlim 8533 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ ((𝐡 +o π‘₯) ∈ V ∧ Lim (𝐡 +o π‘₯))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
229227, 228mpanr1 702 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
230226, 229syl 17 . . . . . . . . . . 11 ((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
231230adantr 482 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
23221ad2antlr 726 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝐴 Β·o 𝐡) ∈ On)
23359jctl 525 . . . . . . . . . . . . . . . 16 (Lim π‘₯ β†’ (π‘₯ ∈ V ∧ Lim π‘₯))
234233anim1ci 617 . . . . . . . . . . . . . . 15 ((Lim π‘₯ ∧ 𝐴 ∈ On) β†’ (𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)))
235 omlimcl 8578 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
236234, 235sylan 581 . . . . . . . . . . . . . 14 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
237236adantlrr 720 . . . . . . . . . . . . 13 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
238 ovex 7442 . . . . . . . . . . . . 13 (𝐴 Β·o π‘₯) ∈ V
239237, 238jctil 521 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o π‘₯) ∈ V ∧ Lim (𝐴 Β·o π‘₯)))
240 oalim 8532 . . . . . . . . . . . 12 (((𝐴 Β·o 𝐡) ∈ On ∧ ((𝐴 Β·o π‘₯) ∈ V ∧ Lim (𝐴 Β·o π‘₯))) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
241232, 239, 240syl2anc 585 . . . . . . . . . . 11 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
242241adantrr 716 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
243221, 231, 2423eqtr4d 2783 . . . . . . . . 9 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))
244243exp43 438 . . . . . . . 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 408 . . . . . 6 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (Lim π‘₯ β†’ (βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
24784, 246oe0lem 8513 . . . . 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 7854 . . 3 (𝐢 ∈ On β†’ ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢))))
250249expdcom 416 . 2 (𝐴 ∈ On β†’ (𝐡 ∈ On β†’ (𝐢 ∈ On β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))))
2512503imp 1112 1 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝐢 ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βŠ† wss 3949  βˆ…c0 4323  βˆͺ ciun 4998  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  (class class class)co 7409   +o coa 8463   Β·o comu 8464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-omul 8471
This theorem is referenced by:  omass  8580  oeeui  8602  oaabs2  8648  oaabsb  42044  naddwordnexlem4  42152
  Copyright terms: Public domain W3C validator