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

Theorem odi 8531
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 7370 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (๐ต +o ๐‘ฅ) = (๐ต +o โˆ…))
21oveq2d 7378 . . . . 5 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo (๐ต +o ๐‘ฅ)) = (๐ด ยทo (๐ต +o โˆ…)))
3 oveq2 7370 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo โˆ…))
43oveq2d 7378 . . . . 5 (๐‘ฅ = โˆ… โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo โˆ…)))
52, 4eqeq12d 2753 . . . 4 (๐‘ฅ = โˆ… โ†’ ((๐ด ยทo (๐ต +o ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) โ†” (๐ด ยทo (๐ต +o โˆ…)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo โˆ…))))
6 oveq2 7370 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐ต +o ๐‘ฅ) = (๐ต +o ๐‘ฆ))
76oveq2d 7378 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด ยทo (๐ต +o ๐‘ฅ)) = (๐ด ยทo (๐ต +o ๐‘ฆ)))
8 oveq2 7370 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo ๐‘ฆ))
98oveq2d 7378 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)))
107, 9eqeq12d 2753 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด ยทo (๐ต +o ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) โ†” (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ))))
11 oveq2 7370 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ต +o ๐‘ฅ) = (๐ต +o suc ๐‘ฆ))
1211oveq2d 7378 . . . . 5 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด ยทo (๐ต +o ๐‘ฅ)) = (๐ด ยทo (๐ต +o suc ๐‘ฆ)))
13 oveq2 7370 . . . . . 6 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo suc ๐‘ฆ))
1413oveq2d 7378 . . . . 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 7370 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ (๐ต +o ๐‘ฅ) = (๐ต +o ๐ถ))
1716oveq2d 7378 . . . . 5 (๐‘ฅ = ๐ถ โ†’ (๐ด ยทo (๐ต +o ๐‘ฅ)) = (๐ด ยทo (๐ต +o ๐ถ)))
18 oveq2 7370 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ (๐ด ยทo ๐‘ฅ) = (๐ด ยทo ๐ถ))
1918oveq2d 7378 . . . . 5 (๐‘ฅ = ๐ถ โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ)))
2017, 19eqeq12d 2753 . . . 4 (๐‘ฅ = ๐ถ โ†’ ((๐ด ยทo (๐ต +o ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) โ†” (๐ด ยทo (๐ต +o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))))
21 omcl 8487 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
22 oa0 8467 . . . . . 6 ((๐ด ยทo ๐ต) โˆˆ On โ†’ ((๐ด ยทo ๐ต) +o โˆ…) = (๐ด ยทo ๐ต))
2321, 22syl 17 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) +o โˆ…) = (๐ด ยทo ๐ต))
24 om0 8468 . . . . . . 7 (๐ด โˆˆ On โ†’ (๐ด ยทo โˆ…) = โˆ…)
2524adantr 482 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo โˆ…) = โˆ…)
2625oveq2d 7378 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo โˆ…)) = ((๐ด ยทo ๐ต) +o โˆ…))
27 oa0 8467 . . . . . . 7 (๐ต โˆˆ On โ†’ (๐ต +o โˆ…) = ๐ต)
2827adantl 483 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ต +o โˆ…) = ๐ต)
2928oveq2d 7378 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo (๐ต +o โˆ…)) = (๐ด ยทo ๐ต))
3023, 26, 293eqtr4rd 2788 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo (๐ต +o โˆ…)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo โˆ…)))
31 oveq1 7369 . . . . . . . 8 ((๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) โ†’ ((๐ด ยทo (๐ต +o ๐‘ฆ)) +o ๐ด) = (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) +o ๐ด))
32 oasuc 8475 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต +o suc ๐‘ฆ) = suc (๐ต +o ๐‘ฆ))
33323adant1 1131 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต +o suc ๐‘ฆ) = suc (๐ต +o ๐‘ฆ))
3433oveq2d 7378 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo (๐ต +o suc ๐‘ฆ)) = (๐ด ยทo suc (๐ต +o ๐‘ฆ)))
35 oacl 8486 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ต +o ๐‘ฆ) โˆˆ On)
36 omsuc 8477 . . . . . . . . . . . 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 2777 . . . . . . . . 9 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo (๐ต +o suc ๐‘ฆ)) = ((๐ด ยทo (๐ต +o ๐‘ฆ)) +o ๐ด))
40 omsuc 8477 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฆ) = ((๐ด ยทo ๐‘ฆ) +o ๐ด))
41403adant2 1132 . . . . . . . . . . 11 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฆ) = ((๐ด ยทo ๐‘ฆ) +o ๐ด))
4241oveq2d 7378 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐‘ฆ) +o ๐ด)))
43 omcl 8487 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฆ) โˆˆ On)
44 oaass 8513 . . . . . . . . . . . . . . . . . 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 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, 54syl5ibr 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 412 . . . 4 (๐‘ฆ โˆˆ On โ†’ ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) โ†’ (๐ด ยทo (๐ต +o suc ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐‘ฆ)))))
59 vex 3452 . . . . . . . . . . . . . 14 ๐‘ฅ โˆˆ V
60 limelon 6386 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ On)
6159, 60mpan 689 . . . . . . . . . . . . 13 (Lim ๐‘ฅ โ†’ ๐‘ฅ โˆˆ On)
62 oacl 8486 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ต +o ๐‘ฅ) โˆˆ On)
63 om0r 8490 . . . . . . . . . . . . . . 15 ((๐ต +o ๐‘ฅ) โˆˆ On โ†’ (โˆ… ยทo (๐ต +o ๐‘ฅ)) = โˆ…)
6462, 63syl 17 . . . . . . . . . . . . . 14 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… ยทo (๐ต +o ๐‘ฅ)) = โˆ…)
65 om0r 8490 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
66 om0r 8490 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ On โ†’ (โˆ… ยทo ๐‘ฅ) = โˆ…)
6765, 66oveqan12d 7381 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ ((โˆ… ยทo ๐ต) +o (โˆ… ยทo ๐‘ฅ)) = (โˆ… +o โˆ…))
68 0elon 6376 . . . . . . . . . . . . . . . 16 โˆ… โˆˆ On
69 oa0 8467 . . . . . . . . . . . . . . . 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 594 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง Lim ๐‘ฅ) โ†’ (โˆ… ยทo (๐ต +o ๐‘ฅ)) = ((โˆ… ยทo ๐ต) +o (โˆ… ยทo ๐‘ฅ)))
7473ancoms 460 . . . . . . . . . . 11 ((Lim ๐‘ฅ โˆง ๐ต โˆˆ On) โ†’ (โˆ… ยทo (๐ต +o ๐‘ฅ)) = ((โˆ… ยทo ๐ต) +o (โˆ… ยทo ๐‘ฅ)))
75 oveq1 7369 . . . . . . . . . . . 12 (๐ด = โˆ… โ†’ (๐ด ยทo (๐ต +o ๐‘ฅ)) = (โˆ… ยทo (๐ต +o ๐‘ฅ)))
76 oveq1 7369 . . . . . . . . . . . . 13 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
77 oveq1 7369 . . . . . . . . . . . . 13 (๐ด = โˆ… โ†’ (๐ด ยทo ๐‘ฅ) = (โˆ… ยทo ๐‘ฅ))
7876, 77oveq12d 7380 . . . . . . . . . . . 12 (๐ด = โˆ… โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) = ((โˆ… ยทo ๐ต) +o (โˆ… ยทo ๐‘ฅ)))
7975, 78eqeq12d 2753 . . . . . . . . . . 11 (๐ด = โˆ… โ†’ ((๐ด ยทo (๐ต +o ๐‘ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฅ)) โ†” (โˆ… ยทo (๐ต +o ๐‘ฅ)) = ((โˆ… ยทo ๐ต) +o (โˆ… ยทo ๐‘ฅ))))
8074, 79syl5ibr 246 . . . . . . . . . 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 6347 . . . . . . . . . . . . . . . . . . . . 21 (((๐ต +o ๐‘ฅ) โˆˆ On โˆง ๐‘ง โˆˆ (๐ต +o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
8886, 87sylan 581 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘ง โˆˆ (๐ต +o ๐‘ฅ)) โ†’ ๐‘ง โˆˆ On)
89 ontri1 6356 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต โˆˆ On โˆง ๐‘ง โˆˆ On) โ†’ (๐ต โŠ† ๐‘ง โ†” ยฌ ๐‘ง โˆˆ ๐ต))
90 oawordex 8509 . . . . . . . . . . . . . . . . . . . . 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 8499 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ฃ โˆˆ On โˆง ๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐‘ฃ โˆˆ ๐‘ฅ โ†” (๐ต +o ๐‘ฃ) โˆˆ (๐ต +o ๐‘ฅ)))
94933expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฃ โˆˆ On โˆง (๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On)) โ†’ (๐‘ฃ โˆˆ ๐‘ฅ โ†” (๐ต +o ๐‘ฃ) โˆˆ (๐ต +o ๐‘ฅ)))
95 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . 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 3163 . . . . . . . . . . . . . . . . . . 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 6385 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Lim ๐‘ฅ โ†’ โˆ… โˆˆ ๐‘ฅ)
112 om00el 8528 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐‘ฅ) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐‘ฅ)))
113112biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8518 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ง โˆˆ ๐ต โ†’ (๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo ๐ต)))
123122ancom1s 652 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ง โˆˆ ๐ต โ†’ (๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo ๐ต)))
124 onelss 6364 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ด ยทo ๐ต) โˆˆ On โ†’ ((๐ด ยทo ๐‘ง) โˆˆ (๐ด ยทo ๐ต) โ†’ (๐ด ยทo ๐‘ง) โŠ† (๐ด ยทo ๐ต)))
12522sseq2d 3981 . . . . . . . . . . . . . . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = โˆ… โ†’ ((๐ด ยทo ๐ต) +o ๐‘ค) = ((๐ด ยทo ๐ต) +o โˆ…))
133132sseq2d 3981 . . . . . . . . . . . . . . . . . . 19 (๐‘ค = โˆ… โ†’ ((๐ด ยทo ๐‘ง) โŠ† ((๐ด ยทo ๐ต) +o ๐‘ค) โ†” (๐ด ยทo ๐‘ง) โŠ† ((๐ด ยทo ๐ต) +o โˆ…)))
134133rspcev 3584 . . . . . . . . . . . . . . . . . 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 8518 . . . . . . . . . . . . . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = ๐‘ฃ โ†’ (๐ต +o ๐‘ฆ) = (๐ต +o ๐‘ฃ))
142141oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = ๐‘ฃ โ†’ (๐ด ยทo (๐ต +o ๐‘ฆ)) = (๐ด ยทo (๐ต +o ๐‘ฃ)))
143 oveq2 7370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = ๐‘ฃ โ†’ (๐ด ยทo ๐‘ฆ) = (๐ด ยทo ๐‘ฃ))
144143oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = ๐‘ฃ โ†’ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ)))
145142, 144eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = ๐‘ฃ โ†’ ((๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) โ†” (๐ด ยทo (๐ต +o ๐‘ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ))))
146145rspccv 3581 . . . . . . . . . . . . . . . . . . . . . 22 (โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) โ†’ (๐‘ฃ โˆˆ ๐‘ฅ โ†’ (๐ด ยทo (๐ต +o ๐‘ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ))))
147 oveq2 7370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐ต +o ๐‘ฃ) = ๐‘ง โ†’ (๐ด ยทo (๐ต +o ๐‘ฃ)) = (๐ด ยทo ๐‘ง))
148 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4006 . . . . . . . . . . . . . . . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ค = (๐ด ยทo ๐‘ฃ) โ†’ ((๐ด ยทo ๐ต) +o ๐‘ค) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ)))
158157sseq2d 3981 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (๐ด ยทo ๐‘ฃ) โ†’ ((๐ด ยทo ๐‘ง) โŠ† ((๐ด ยทo ๐ต) +o ๐‘ค) โ†” (๐ด ยทo ๐‘ง) โŠ† ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ))))
159158rspcev 3584 . . . . . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . . . . 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 3144 . . . . . . . . . . . 12 (((Lim ๐‘ฅ โˆง (๐ด โˆˆ On โˆง ๐ต โˆˆ On)) โˆง (โˆ… โˆˆ ๐ด โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)))) โ†’ โˆ€๐‘ง โˆˆ (๐ต +o ๐‘ฅ)โˆƒ๐‘ค โˆˆ (๐ด ยทo ๐‘ฅ)(๐ด ยทo ๐‘ง) โŠ† ((๐ด ยทo ๐ต) +o ๐‘ค))
167 iunss2 5014 . . . . . . . . . . . 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 8529 . . . . . . . . . . . . . . . . . . . . 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 8498 . . . . . . . . . . . . . . . . . . . . . . . 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 6382 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Lim ๐‘ฅ โ†’ Ord ๐‘ฅ)
183 ordelon 6346 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Ord ๐‘ฅ โˆง ๐‘ฃ โˆˆ ๐‘ฅ) โ†’ ๐‘ฃ โˆˆ On)
184182, 183sylan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Lim ๐‘ฅ โˆง ๐‘ฃ โˆˆ ๐‘ฅ) โ†’ ๐‘ฃ โˆˆ On)
185 omcl 8487 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8498 . . . . . . . . . . . . . . . . . . . . . . . . 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 3583 . . . . . . . . . . . . . . . . . . . . . . 23 ((โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)) โˆง ๐‘ฃ โˆˆ ๐‘ฅ) โ†’ (๐ด ยทo (๐ต +o ๐‘ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฃ)))
195194eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . 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 8486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐ต โˆˆ On โˆง ๐‘ฃ โˆˆ On) โ†’ (๐ต +o ๐‘ฃ) โˆˆ On)
199198ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฃ โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ต +o ๐‘ฃ) โˆˆ On)
200 omcl 8487 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6364 . . . . . . . . . . . . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง = (๐ต +o ๐‘ฃ) โ†’ (๐ด ยทo ๐‘ง) = (๐ด ยทo (๐ต +o ๐‘ฃ)))
211210sseq2d 3981 . . . . . . . . . . . . . . . . . . 19 (๐‘ง = (๐ต +o ๐‘ฃ) โ†’ (((๐ด ยทo ๐ต) +o ๐‘ค) โŠ† (๐ด ยทo ๐‘ง) โ†” ((๐ด ยทo ๐ต) +o ๐‘ค) โŠ† (๐ด ยทo (๐ต +o ๐‘ฃ))))
212211rspcev 3584 . . . . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . . . 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 3144 . . . . . . . . . . . . 13 (((Lim ๐‘ฅ โˆง (๐ด โˆˆ On โˆง ๐ต โˆˆ On)) โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ))) โ†’ โˆ€๐‘ค โˆˆ (๐ด ยทo ๐‘ฅ)โˆƒ๐‘ง โˆˆ (๐ต +o ๐‘ฅ)((๐ด ยทo ๐ต) +o ๐‘ค) โŠ† (๐ด ยทo ๐‘ง))
218 iunss2 5014 . . . . . . . . . . . . 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 3966 . . . . . . . . . 10 (((Lim ๐‘ฅ โˆง (๐ด โˆˆ On โˆง ๐ต โˆˆ On)) โˆง (โˆ… โˆˆ ๐ด โˆง โˆ€๐‘ฆ โˆˆ ๐‘ฅ (๐ด ยทo (๐ต +o ๐‘ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐‘ฆ)))) โ†’ โˆช ๐‘ง โˆˆ (๐ต +o ๐‘ฅ)(๐ด ยทo ๐‘ง) = โˆช ๐‘ค โˆˆ (๐ด ยทo ๐‘ฅ)((๐ด ยทo ๐ต) +o ๐‘ค))
222 oalimcl 8512 . . . . . . . . . . . . . . . 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 7395 . . . . . . . . . . . . 13 (๐ต +o ๐‘ฅ) โˆˆ V
228 omlim 8484 . . . . . . . . . . . . 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 8530 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง (๐‘ฅ โˆˆ V โˆง Lim ๐‘ฅ)) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐‘ฅ))
236234, 235sylan 581 . . . . . . . . . . . . . 14 (((Lim ๐‘ฅ โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐‘ฅ))
237236adantlrr 720 . . . . . . . . . . . . 13 (((Lim ๐‘ฅ โˆง (๐ด โˆˆ On โˆง ๐ต โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ Lim (๐ด ยทo ๐‘ฅ))
238 ovex 7395 . . . . . . . . . . . . 13 (๐ด ยทo ๐‘ฅ) โˆˆ V
239237, 238jctil 521 . . . . . . . . . . . 12 (((Lim ๐‘ฅ โˆง (๐ด โˆˆ On โˆง ๐ต โˆˆ On)) โˆง โˆ… โˆˆ ๐ด) โ†’ ((๐ด ยทo ๐‘ฅ) โˆˆ V โˆง Lim (๐ด ยทo ๐‘ฅ)))
240 oalim 8483 . . . . . . . . . . . 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 2787 . . . . . . . . 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 8464 . . . . 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 7806 . . 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 3065  โˆƒwrex 3074  Vcvv 3448   โŠ† wss 3915  โˆ…c0 4287  โˆช ciun 4959  Ord word 6321  Oncon0 6322  Lim wlim 6323  suc csuc 6324  (class class class)co 7362   +o coa 8414   ยทo comu 8415
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-omul 8422
This theorem is referenced by:  omass  8532  oeeui  8554  oaabs2  8600  oaabsb  41658  naddwordnexlem4  41747
  Copyright terms: Public domain W3C validator