MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  odi Structured version   Visualization version   GIF version
Theorem odi 8598
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 7425 . . . . . 6 (π‘₯ = βˆ… β†’ (𝐡 +o π‘₯) = (𝐡 +o βˆ…))
21oveq2d 7433 . . . . 5 (π‘₯ = βˆ… β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o βˆ…)))
3 oveq2 7425 . . . . . 6 (π‘₯ = βˆ… β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o βˆ…))
43oveq2d 7433 . . . . 5 (π‘₯ = βˆ… β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)))
52, 4eqeq12d 2741 . . . 4 (π‘₯ = βˆ… β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o βˆ…)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…))))
6 oveq2 7425 . . . . . 6 (π‘₯ = 𝑦 β†’ (𝐡 +o π‘₯) = (𝐡 +o 𝑦))
76oveq2d 7433 . . . . 5 (π‘₯ = 𝑦 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o 𝑦)))
8 oveq2 7425 . . . . . 6 (π‘₯ = 𝑦 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o 𝑦))
98oveq2d 7433 . . . . 5 (π‘₯ = 𝑦 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))
107, 9eqeq12d 2741 . . . 4 (π‘₯ = 𝑦 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))))
11 oveq2 7425 . . . . . 6 (π‘₯ = suc 𝑦 β†’ (𝐡 +o π‘₯) = (𝐡 +o suc 𝑦))
1211oveq2d 7433 . . . . 5 (π‘₯ = suc 𝑦 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o suc 𝑦)))
13 oveq2 7425 . . . . . 6 (π‘₯ = suc 𝑦 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o suc 𝑦))
1413oveq2d 7433 . . . . 5 (π‘₯ = suc 𝑦 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)))
1512, 14eqeq12d 2741 . . . 4 (π‘₯ = suc 𝑦 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦))))
16 oveq2 7425 . . . . . 6 (π‘₯ = 𝐢 β†’ (𝐡 +o π‘₯) = (𝐡 +o 𝐢))
1716oveq2d 7433 . . . . 5 (π‘₯ = 𝐢 β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (𝐴 Β·o (𝐡 +o 𝐢)))
18 oveq2 7425 . . . . . 6 (π‘₯ = 𝐢 β†’ (𝐴 Β·o π‘₯) = (𝐴 Β·o 𝐢))
1918oveq2d 7433 . . . . 5 (π‘₯ = 𝐢 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))
2017, 19eqeq12d 2741 . . . 4 (π‘₯ = 𝐢 β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢))))
21 omcl 8555 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o 𝐡) ∈ On)
22 oa0 8535 . . . . . 6 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝐡) +o βˆ…) = (𝐴 Β·o 𝐡))
2321, 22syl 17 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o βˆ…) = (𝐴 Β·o 𝐡))
24 om0 8536 . . . . . . 7 (𝐴 ∈ On β†’ (𝐴 Β·o βˆ…) = βˆ…)
2524adantr 479 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o βˆ…) = βˆ…)
2625oveq2d 7433 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)) = ((𝐴 Β·o 𝐡) +o βˆ…))
27 oa0 8535 . . . . . . 7 (𝐡 ∈ On β†’ (𝐡 +o βˆ…) = 𝐡)
2827adantl 480 . . . . . 6 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o βˆ…) = 𝐡)
2928oveq2d 7433 . . . . 5 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o βˆ…)) = (𝐴 Β·o 𝐡))
3023, 26, 293eqtr4rd 2776 . . . 4 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o βˆ…)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o βˆ…)))
31 oveq1 7424 . . . . . . . 8 ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴) = (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴))
32 oasuc 8543 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o suc 𝑦) = suc (𝐡 +o 𝑦))
33323adant1 1127 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o suc 𝑦) = suc (𝐡 +o 𝑦))
3433oveq2d 7433 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = (𝐴 Β·o suc (𝐡 +o 𝑦)))
35 oacl 8554 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐡 +o 𝑦) ∈ On)
36 omsuc 8545 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐡 +o 𝑦) ∈ On) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
3735, 36sylan2 591 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝐡 ∈ On ∧ 𝑦 ∈ On)) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
38373impb 1112 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc (𝐡 +o 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
3934, 38eqtrd 2765 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o (𝐡 +o 𝑦)) +o 𝐴))
40 omsuc 8545 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc 𝑦) = ((𝐴 Β·o 𝑦) +o 𝐴))
41403adant2 1128 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o suc 𝑦) = ((𝐴 Β·o 𝑦) +o 𝐴))
4241oveq2d 7433 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
43 omcl 8555 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 Β·o 𝑦) ∈ On)
44 oaass 8580 . . . . . . . . . . . . . . . . . 18 (((𝐴 Β·o 𝐡) ∈ On ∧ (𝐴 Β·o 𝑦) ∈ On ∧ 𝐴 ∈ On) β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
4521, 44syl3an1 1160 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ (𝐴 Β·o 𝑦) ∈ On ∧ 𝐴 ∈ On) β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
4643, 45syl3an2 1161 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ (𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ∈ On) β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
47463exp 1116 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 ∈ On ∧ 𝑦 ∈ On) β†’ (𝐴 ∈ On β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))))
4847exp4b 429 . . . . . . . . . . . . . 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 1108 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴) = ((𝐴 Β·o 𝐡) +o ((𝐴 Β·o 𝑦) +o 𝐴)))
5342, 52eqtr4d 2768 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝑦 ∈ On) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)) = (((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) +o 𝐴))
5439, 53eqeq12d 2741 . . . . . . . 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 1116 . . . . . 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 409 . . . 4 (𝑦 ∈ On β†’ ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝐴 Β·o (𝐡 +o suc 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o suc 𝑦)))))
59 vex 3467 . . . . . . . . . . . . . 14 π‘₯ ∈ V
60 limelon 6433 . . . . . . . . . . . . . 14 ((π‘₯ ∈ V ∧ Lim π‘₯) β†’ π‘₯ ∈ On)
6159, 60mpan 688 . . . . . . . . . . . . 13 (Lim π‘₯ β†’ π‘₯ ∈ On)
62 oacl 8554 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (𝐡 +o π‘₯) ∈ On)
63 om0r 8558 . . . . . . . . . . . . . . 15 ((𝐡 +o π‘₯) ∈ On β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = βˆ…)
6462, 63syl 17 . . . . . . . . . . . . . 14 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = βˆ…)
65 om0r 8558 . . . . . . . . . . . . . . . 16 (𝐡 ∈ On β†’ (βˆ… Β·o 𝐡) = βˆ…)
66 om0r 8558 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ On β†’ (βˆ… Β·o π‘₯) = βˆ…)
6765, 66oveqan12d 7436 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)) = (βˆ… +o βˆ…))
68 0elon 6423 . . . . . . . . . . . . . . . 16 βˆ… ∈ On
69 oa0 8535 . . . . . . . . . . . . . . . 16 (βˆ… ∈ On β†’ (βˆ… +o βˆ…) = βˆ…)
7068, 69ax-mp 5 . . . . . . . . . . . . . . 15 (βˆ… +o βˆ…) = βˆ…
7167, 70eqtr2di 2782 . . . . . . . . . . . . . 14 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ βˆ… = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7264, 71eqtrd 2765 . . . . . . . . . . . . 13 ((𝐡 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7361, 72sylan2 591 . . . . . . . . . . . 12 ((𝐡 ∈ On ∧ Lim π‘₯) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7473ancoms 457 . . . . . . . . . . 11 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
75 oveq1 7424 . . . . . . . . . . . 12 (𝐴 = βˆ… β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = (βˆ… Β·o (𝐡 +o π‘₯)))
76 oveq1 7424 . . . . . . . . . . . . 13 (𝐴 = βˆ… β†’ (𝐴 Β·o 𝐡) = (βˆ… Β·o 𝐡))
77 oveq1 7424 . . . . . . . . . . . . 13 (𝐴 = βˆ… β†’ (𝐴 Β·o π‘₯) = (βˆ… Β·o π‘₯))
7876, 77oveq12d 7435 . . . . . . . . . . . 12 (𝐴 = βˆ… β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯)))
7975, 78eqeq12d 2741 . . . . . . . . . . 11 (𝐴 = βˆ… β†’ ((𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) ↔ (βˆ… Β·o (𝐡 +o π‘₯)) = ((βˆ… Β·o 𝐡) +o (βˆ… Β·o π‘₯))))
8074, 79imbitrrid 245 . . . . . . . . . 10 (𝐴 = βˆ… β†’ ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯))))
8180expd 414 . . . . . . . . 9 (𝐴 = βˆ… β†’ (Lim π‘₯ β†’ (𝐡 ∈ On β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
8281com3r 87 . . . . . . . 8 (𝐡 ∈ On β†’ (𝐴 = βˆ… β†’ (Lim π‘₯ β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
8382imp 405 . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝐡 ∈ On)
8662ancoms 457 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o π‘₯) ∈ On)
87 onelon 6394 . . . . . . . . . . . . . . . . . . . . 21 (((𝐡 +o π‘₯) ∈ On ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝑧 ∈ On)
8886, 87sylan 578 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ 𝑧 ∈ On)
89 ontri1 6403 . . . . . . . . . . . . . . . . . . . . 21 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (𝐡 βŠ† 𝑧 ↔ Β¬ 𝑧 ∈ 𝐡))
90 oawordex 8576 . . . . . . . . . . . . . . . . . . . . 21 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (𝐡 βŠ† 𝑧 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
9189, 90bitr3d 280 . . . . . . . . . . . . . . . . . . . 20 ((𝐡 ∈ On ∧ 𝑧 ∈ On) β†’ (Β¬ 𝑧 ∈ 𝐡 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
9285, 88, 91syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (Β¬ 𝑧 ∈ 𝐡 ↔ βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧))
93 oaord 8566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ On ∧ π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ ↔ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
94933expb 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑣 ∈ π‘₯ ↔ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
95 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 +o 𝑣) = 𝑧 β†’ ((𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯) ↔ 𝑧 ∈ (𝐡 +o π‘₯)))
9694, 95sylan9bb 508 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑣 ∈ π‘₯ ↔ 𝑧 ∈ (𝐡 +o π‘₯)))
97 iba 526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
9897adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑣 ∈ π‘₯ ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
9996, 98bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑣 ∈ On ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝑧 ∈ (𝐡 +o π‘₯) ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10099an32s 650 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑣 ∈ On ∧ (𝐡 +o 𝑣) = 𝑧) ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑧 ∈ (𝐡 +o π‘₯) ↔ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
101100biimpcd 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐡 +o π‘₯) β†’ (((𝑣 ∈ On ∧ (𝐡 +o 𝑣) = 𝑧) ∧ (π‘₯ ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
102101exp4c 431 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐡 +o π‘₯) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))))
103102com4r 94 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑧 ∈ (𝐡 +o π‘₯) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))))
104103imp 405 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑣 ∈ On β†’ ((𝐡 +o 𝑣) = 𝑧 β†’ (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧))))
105104reximdvai 3155 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (βˆƒπ‘£ ∈ On (𝐡 +o 𝑣) = 𝑧 β†’ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10692, 105sylbid 239 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (Β¬ 𝑧 ∈ 𝐡 β†’ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
107106orrd 861 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ On ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
10861, 107sylanl1 678 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ 𝐡 ∈ On) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
109108adantlrl 718 . . . . . . . . . . . . . . 15 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
110109adantlr 713 . . . . . . . . . . . . . 14 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) ∧ 𝑧 ∈ (𝐡 +o π‘₯)) β†’ (𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)))
111 0ellim 6432 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Lim π‘₯ β†’ βˆ… ∈ π‘₯)
112 om00el 8595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ (βˆ… ∈ (𝐴 Β·o π‘₯) ↔ (βˆ… ∈ 𝐴 ∧ βˆ… ∈ π‘₯)))
113112biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… ∈ 𝐴 ∧ βˆ… ∈ π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
114111, 113sylan2i 604 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ π‘₯ ∈ On) β†’ ((βˆ… ∈ 𝐴 ∧ Lim π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
11561, 114sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ Lim π‘₯) β†’ ((βˆ… ∈ 𝐴 ∧ Lim π‘₯) β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
116115exp4b 429 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On β†’ (Lim π‘₯ β†’ (βˆ… ∈ 𝐴 β†’ (Lim π‘₯ β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))))
117116com4r 94 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim π‘₯ β†’ (𝐴 ∈ On β†’ (Lim π‘₯ β†’ (βˆ… ∈ 𝐴 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))))
118117pm2.43a 54 . . . . . . . . . . . . . . . . . . . . . 22 (Lim π‘₯ β†’ (𝐴 ∈ On β†’ (βˆ… ∈ 𝐴 β†’ βˆ… ∈ (𝐴 Β·o π‘₯))))
119118imp31 416 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ βˆ… ∈ (𝐴 Β·o π‘₯))
120119a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
121120adantlrr 719 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆ… ∈ (𝐴 Β·o π‘₯)))
122 omordi 8585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐡 ∈ On ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡)))
123122ancom1s 651 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡)))
124 onelss 6411 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† (𝐴 Β·o 𝐡)))
12522sseq2d 4010 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…) ↔ (𝐴 Β·o 𝑧) βŠ† (𝐴 Β·o 𝐡)))
126124, 125sylibrd 258 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 Β·o 𝐡) ∈ On β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
12721, 126syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
128127adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o 𝑧) ∈ (𝐴 Β·o 𝐡) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
129123, 128syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
130129adantll 712 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
131121, 130jcad 511 . . . . . . . . . . . . . . . . . 18 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ (βˆ… ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…))))
132 oveq2 7425 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = βˆ… β†’ ((𝐴 Β·o 𝐡) +o 𝑀) = ((𝐴 Β·o 𝐡) +o βˆ…))
133132sseq2d 4010 . . . . . . . . . . . . . . . . . . 19 (𝑀 = βˆ… β†’ ((𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀) ↔ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)))
134133rspcev 3607 . . . . . . . . . . . . . . . . . 18 ((βˆ… ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o βˆ…)) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀))
135131, 134syl6 35 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝑧 ∈ 𝐡 β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
136135adantrr 715 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝑧 ∈ 𝐡 β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
137 omordi 8585 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘₯ ∈ On ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
13861, 137sylanl1 678 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
139138adantrd 490 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
140139adantrr 715 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯)))
141 oveq2 7425 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 β†’ (𝐡 +o 𝑦) = (𝐡 +o 𝑣))
142141oveq2d 7433 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 β†’ (𝐴 Β·o (𝐡 +o 𝑦)) = (𝐴 Β·o (𝐡 +o 𝑣)))
143 oveq2 7425 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑣 β†’ (𝐴 Β·o 𝑦) = (𝐴 Β·o 𝑣))
144143oveq2d 7433 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
145142, 144eqeq12d 2741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑣 β†’ ((𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ↔ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
146145rspccv 3604 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝑣 ∈ π‘₯ β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
147 oveq2 7425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐡 +o 𝑣) = 𝑧 β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = (𝐴 Β·o 𝑧))
148 eqeq1 2729 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4037 . . . . . . . . . . . . . . . . . . . . . . . . 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 409 . . . . . . . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
156140, 155jcad 511 . . . . . . . . . . . . . . . . . . 19 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ ((𝐴 Β·o 𝑣) ∈ (𝐴 Β·o π‘₯) ∧ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))))
157 oveq2 7425 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
158157sseq2d 4010 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀) ↔ (𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
159158rspcev 3607 . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
162161adantlrr 719 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
163136, 162jaod 857 . . . . . . . . . . . . . . 15 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝑧 ∈ 𝐡 ∨ βˆƒπ‘£ ∈ On (𝑣 ∈ π‘₯ ∧ (𝐡 +o 𝑣) = 𝑧)) β†’ βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀)))
164163adantr 479 . . . . . . . . . . . . . 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 3136 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆ€π‘§ ∈ (𝐡 +o π‘₯)βˆƒπ‘€ ∈ (𝐴 Β·o π‘₯)(𝐴 Β·o 𝑧) βŠ† ((𝐴 Β·o 𝐡) +o 𝑀))
167 iunss2 5052 . . . . . . . . . . . 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 8596 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
170169ex 411 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
17159, 170mpanr1 701 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ Lim π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
172171ancoms 457 . . . . . . . . . . . . . . . . . 18 ((Lim π‘₯ ∧ 𝐴 ∈ On) β†’ (𝑀 ∈ (𝐴 Β·o π‘₯) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣)))
173172imp 405 . . . . . . . . . . . . . . . . 17 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
174173adantlrr 719 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
175174adantlr 713 . . . . . . . . . . . . . . 15 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑀 ∈ (𝐴 Β·o π‘₯)) β†’ βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣))
176 oaordi 8565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
17761, 176sylan 578 . . . . . . . . . . . . . . . . . . . . . . 23 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ (𝑣 ∈ π‘₯ β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
178177imp 405 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ 𝐡 ∈ On) ∧ 𝑣 ∈ π‘₯) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯))
179178adantlrl 718 . . . . . . . . . . . . . . . . . . . . 21 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯))
180179a1d 25 . . . . . . . . . . . . . . . . . . . 20 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
181180adantlr 713 . . . . . . . . . . . . . . . . . . 19 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ (𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯)))
182 limord 6429 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim π‘₯ β†’ Ord π‘₯)
183 ordelon 6393 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord π‘₯ ∧ 𝑣 ∈ π‘₯) β†’ 𝑣 ∈ On)
184182, 183sylan 578 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) β†’ 𝑣 ∈ On)
185 omcl 8555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ 𝑣 ∈ On) β†’ (𝐴 Β·o 𝑣) ∈ On)
186185ancoms 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐴 ∈ On) β†’ (𝐴 Β·o 𝑣) ∈ On)
187186adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o 𝑣) ∈ On)
18821adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o 𝐡) ∈ On)
189 oaordi 8565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 Β·o 𝑣) ∈ On ∧ (𝐴 Β·o 𝐡) ∈ On) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
190187, 188, 189syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
191184, 190sylan 578 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
192191an32s 650 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
193192adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
194145rspccva 3606 . . . . . . . . . . . . . . . . . . . . . . 23 ((βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣)))
195194eleq2d 2811 . . . . . . . . . . . . . . . . . . . . . 22 ((βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) ∧ 𝑣 ∈ π‘₯) β†’ (((𝐴 Β·o 𝐡) +o 𝑀) ∈ (𝐴 Β·o (𝐡 +o 𝑣)) ↔ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
196195adantll 712 . . . . . . . . . . . . . . . . . . . . 21 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (((𝐴 Β·o 𝐡) +o 𝑀) ∈ (𝐴 Β·o (𝐡 +o 𝑣)) ↔ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑣))))
197193, 196sylibrd 258 . . . . . . . . . . . . . . . . . . . 20 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐴 Β·o 𝐡) +o 𝑀) ∈ (𝐴 Β·o (𝐡 +o 𝑣))))
198 oacl 8554 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐡 ∈ On ∧ 𝑣 ∈ On) β†’ (𝐡 +o 𝑣) ∈ On)
199198ancoms 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐡 +o 𝑣) ∈ On)
200 omcl 8555 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ On ∧ (𝐡 +o 𝑣) ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
201199, 200sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
202201an12s 647 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
203184, 202sylan 578 . . . . . . . . . . . . . . . . . . . . . . 23 (((Lim π‘₯ ∧ 𝑣 ∈ π‘₯) ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
204203an32s 650 . . . . . . . . . . . . . . . . . . . . . 22 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ 𝑣 ∈ π‘₯) β†’ (𝐴 Β·o (𝐡 +o 𝑣)) ∈ On)
205 onelss 6411 . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . 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 511 . . . . . . . . . . . . . . . . . 18 ((((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) ∧ 𝑣 ∈ π‘₯) β†’ (𝑀 ∈ (𝐴 Β·o 𝑣) β†’ ((𝐡 +o 𝑣) ∈ (𝐡 +o π‘₯) ∧ ((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o (𝐡 +o 𝑣)))))
210 oveq2 7425 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝐡 +o 𝑣) β†’ (𝐴 Β·o 𝑧) = (𝐴 Β·o (𝐡 +o 𝑣)))
211210sseq2d 4010 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐡 +o 𝑣) β†’ (((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧) ↔ ((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o (𝐡 +o 𝑣))))
212211rspcev 3607 . . . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . . 16 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) β†’ (βˆƒπ‘£ ∈ π‘₯ 𝑀 ∈ (𝐴 Β·o 𝑣) β†’ βˆƒπ‘§ ∈ (𝐡 +o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧)))
215214adantr 479 . . . . . . . . . . . . . . 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 3136 . . . . . . . . . . . . 13 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦))) β†’ βˆ€π‘€ ∈ (𝐴 Β·o π‘₯)βˆƒπ‘§ ∈ (𝐡 +o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† (𝐴 Β·o 𝑧))
218 iunss2 5052 . . . . . . . . . . . . 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 714 . . . . . . . . . . 11 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀) βŠ† βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
221168, 220eqssd 3995 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
222 oalimcl 8579 . . . . . . . . . . . . . . . 16 ((𝐡 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) β†’ Lim (𝐡 +o π‘₯))
22359, 222mpanr1 701 . . . . . . . . . . . . . . 15 ((𝐡 ∈ On ∧ Lim π‘₯) β†’ Lim (𝐡 +o π‘₯))
224223ancoms 457 . . . . . . . . . . . . . 14 ((Lim π‘₯ ∧ 𝐡 ∈ On) β†’ Lim (𝐡 +o π‘₯))
225224anim2i 615 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (Lim π‘₯ ∧ 𝐡 ∈ On)) β†’ (𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)))
226225an12s 647 . . . . . . . . . . . 12 ((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)))
227 ovex 7450 . . . . . . . . . . . . 13 (𝐡 +o π‘₯) ∈ V
228 omlim 8552 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ ((𝐡 +o π‘₯) ∈ V ∧ Lim (𝐡 +o π‘₯))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
229227, 228mpanr1 701 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ Lim (𝐡 +o π‘₯)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
230226, 229syl 17 . . . . . . . . . . 11 ((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
231230adantr 479 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = βˆͺ 𝑧 ∈ (𝐡 +o π‘₯)(𝐴 Β·o 𝑧))
23221ad2antlr 725 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ (𝐴 Β·o 𝐡) ∈ On)
23359jctl 522 . . . . . . . . . . . . . . . 16 (Lim π‘₯ β†’ (π‘₯ ∈ V ∧ Lim π‘₯))
234233anim1ci 614 . . . . . . . . . . . . . . 15 ((Lim π‘₯ ∧ 𝐴 ∈ On) β†’ (𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)))
235 omlimcl 8597 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ (π‘₯ ∈ V ∧ Lim π‘₯)) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
236234, 235sylan 578 . . . . . . . . . . . . . 14 (((Lim π‘₯ ∧ 𝐴 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
237236adantlrr 719 . . . . . . . . . . . . 13 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ Lim (𝐴 Β·o π‘₯))
238 ovex 7450 . . . . . . . . . . . . 13 (𝐴 Β·o π‘₯) ∈ V
239237, 238jctil 518 . . . . . . . . . . . 12 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o π‘₯) ∈ V ∧ Lim (𝐴 Β·o π‘₯)))
240 oalim 8551 . . . . . . . . . . . 12 (((𝐴 Β·o 𝐡) ∈ On ∧ ((𝐴 Β·o π‘₯) ∈ V ∧ Lim (𝐴 Β·o π‘₯))) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
241232, 239, 240syl2anc 582 . . . . . . . . . . 11 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ βˆ… ∈ 𝐴) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
242241adantrr 715 . . . . . . . . . 10 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)) = βˆͺ 𝑀 ∈ (𝐴 Β·o π‘₯)((𝐴 Β·o 𝐡) +o 𝑀))
243221, 231, 2423eqtr4d 2775 . . . . . . . . 9 (((Lim π‘₯ ∧ (𝐴 ∈ On ∧ 𝐡 ∈ On)) ∧ (βˆ… ∈ 𝐴 ∧ βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)))) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))
244243exp43 435 . . . . . . . 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 405 . . . . . 6 (((𝐴 ∈ On ∧ 𝐡 ∈ On) ∧ βˆ… ∈ 𝐴) β†’ (Lim π‘₯ β†’ (βˆ€π‘¦ ∈ π‘₯ (𝐴 Β·o (𝐡 +o 𝑦)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝑦)) β†’ (𝐴 Β·o (𝐡 +o π‘₯)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o π‘₯)))))
24784, 246oe0lem 8532 . . . . 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 7868 . . 3 (𝐢 ∈ On β†’ ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢))))
250249expdcom 413 . 2 (𝐴 ∈ On β†’ (𝐡 ∈ On β†’ (𝐢 ∈ On β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))))
2512503imp 1108 1 ((𝐴 ∈ On ∧ 𝐡 ∈ On ∧ 𝐢 ∈ On) β†’ (𝐴 Β·o (𝐡 +o 𝐢)) = ((𝐴 Β·o 𝐡) +o (𝐴 Β·o 𝐢)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  βˆƒwrex 3060  Vcvv 3463   βŠ† wss 3945  βˆ…c0 4323  βˆͺ ciun 4996  Ord word 6368  Oncon0 6369  Lim wlim 6370  suc csuc 6371  (class class class)co 7417   +o coa 8482   Β·o comu 8483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  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 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-oadd 8489  df-omul 8490
This theorem is referenced by:  omass  8599  oeeui  8621  oaabs2  8668  oaabsb  42788  naddwordnexlem4  42896
  Copyright terms: Public domain W3C validator