Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ต +o ๐ฅ) = (๐ต +o โ
)) |
2 | 1 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = โ
โ (๐ด ยทo (๐ต +o ๐ฅ)) = (๐ด ยทo (๐ต +o โ
))) |
3 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด ยทo ๐ฅ) = (๐ด ยทo
โ
)) |
4 | 3 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo
โ
))) |
5 | 2, 4 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = โ
โ ((๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) โ (๐ด ยทo (๐ต +o โ
)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo
โ
)))) |
6 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ต +o ๐ฅ) = (๐ต +o ๐ฆ)) |
7 | 6 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด ยทo (๐ต +o ๐ฅ)) = (๐ด ยทo (๐ต +o ๐ฆ))) |
8 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ฆ)) |
9 | 8 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) |
10 | 7, 9 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) โ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) |
11 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ต +o ๐ฅ) = (๐ต +o suc ๐ฆ)) |
12 | 11 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo (๐ต +o ๐ฅ)) = (๐ด ยทo (๐ต +o suc ๐ฆ))) |
13 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo suc ๐ฆ)) |
14 | 13 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ))) |
15 | 12, 14 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) โ (๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)))) |
16 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ต +o ๐ฅ) = (๐ต +o ๐ถ)) |
17 | 16 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ถ โ (๐ด ยทo (๐ต +o ๐ฅ)) = (๐ด ยทo (๐ต +o ๐ถ))) |
18 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ถ)) |
19 | 18 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ถ โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
20 | 17, 19 | eqeq12d 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
๐ต)) |
23 | 21, 22 | syl 17 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) +o โ
) =
(๐ด ยทo
๐ต)) |
24 | | om0 8468 |
. . . . . . 7
โข (๐ด โ On โ (๐ด ยทo โ
) =
โ
) |
25 | 24 | adantr 482 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo โ
) =
โ
) |
26 | 25 | oveq2d 7378 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo โ
))
= ((๐ด ยทo
๐ต) +o
โ
)) |
27 | | oa0 8467 |
. . . . . . 7
โข (๐ต โ On โ (๐ต +o โ
) = ๐ต) |
28 | 27 | adantl 483 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (๐ต +o โ
) = ๐ต) |
29 | 28 | oveq2d 7378 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo (๐ต +o โ
)) =
(๐ด ยทo
๐ต)) |
30 | 23, 26, 29 | 3eqtr4rd 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 ๐ฆ)) |
33 | 32 | 3adant1 1131 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต +o suc ๐ฆ) = suc (๐ต +o ๐ฆ)) |
34 | 33 | oveq2d 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 ๐ด)) |
37 | 35, 36 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ด โ On โง (๐ต โ On โง ๐ฆ โ On)) โ (๐ด ยทo suc (๐ต +o ๐ฆ)) = ((๐ด ยทo (๐ต +o ๐ฆ)) +o ๐ด)) |
38 | 37 | 3impb 1116 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo suc (๐ต +o ๐ฆ)) = ((๐ด ยทo (๐ต +o ๐ฆ)) +o ๐ด)) |
39 | 34, 38 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo (๐ต +o ๐ฆ)) +o ๐ด)) |
40 | | omsuc 8477 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
41 | 40 | 3adant2 1132 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
42 | 41 | oveq2d 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 ๐ด))) |
45 | 21, 44 | syl3an1 1164 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ On โง ๐ต โ On) โง (๐ด ยทo ๐ฆ) โ On โง ๐ด โ On) โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))) |
46 | 43, 45 | syl3an2 1165 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ On โง ๐ต โ On) โง (๐ด โ On โง ๐ฆ โ On) โง ๐ด โ On) โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))) |
47 | 46 | 3exp 1120 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โ On โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))))) |
48 | 47 | exp4b 432 |
. . . . . . . . . . . . . 14
โข (๐ด โ On โ (๐ต โ On โ (๐ด โ On โ (๐ฆ โ On โ (๐ด โ On โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))))))) |
49 | 48 | pm2.43a 54 |
. . . . . . . . . . . . 13
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ด โ On โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด)))))) |
50 | 49 | com4r 94 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด)))))) |
51 | 50 | pm2.43i 52 |
. . . . . . . . . . 11
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))))) |
52 | 51 | 3imp 1112 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด) = ((๐ด ยทo ๐ต) +o ((๐ด ยทo ๐ฆ) +o ๐ด))) |
53 | 42, 52 | eqtr4d 2780 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)) = (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด)) |
54 | 39, 53 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)) โ ((๐ด ยทo (๐ต +o ๐ฆ)) +o ๐ด) = (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) +o ๐ด))) |
55 | 31, 54 | syl5ibr 246 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)))) |
56 | 55 | 3exp 1120 |
. . . . . 6
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ ((๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)))))) |
57 | 56 | com3r 87 |
. . . . 5
โข (๐ฆ โ On โ (๐ด โ On โ (๐ต โ On โ ((๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o suc ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo suc ๐ฆ)))))) |
58 | 57 | impd 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) |
61 | 59, 60 | mpan 689 |
. . . . . . . . . . . . 13
โข (Lim
๐ฅ โ ๐ฅ โ On) |
62 | | oacl 8486 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ On โง ๐ฅ โ On) โ (๐ต +o ๐ฅ) โ On) |
63 | | om0r 8490 |
. . . . . . . . . . . . . . 15
โข ((๐ต +o ๐ฅ) โ On โ (โ
ยทo (๐ต
+o ๐ฅ)) =
โ
) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง ๐ฅ โ On) โ (โ
ยทo (๐ต
+o ๐ฅ)) =
โ
) |
65 | | om0r 8490 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
66 | | om0r 8490 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ On โ (โ
ยทo ๐ฅ) =
โ
) |
67 | 65, 66 | oveqan12d 7381 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ On โง ๐ฅ โ On) โ ((โ
ยทo ๐ต)
+o (โ
ยทo ๐ฅ)) = (โ
+o
โ
)) |
68 | | 0elon 6376 |
. . . . . . . . . . . . . . . 16
โข โ
โ On |
69 | | oa0 8467 |
. . . . . . . . . . . . . . . 16
โข (โ
โ On โ (โ
+o โ
) = โ
) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (โ
+o โ
) = โ
|
71 | 67, 70 | eqtr2di 2794 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง ๐ฅ โ On) โ โ
=
((โ
ยทo ๐ต) +o (โ
ยทo ๐ฅ))) |
72 | 64, 71 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ฅ โ On) โ (โ
ยทo (๐ต
+o ๐ฅ)) =
((โ
ยทo ๐ต) +o (โ
ยทo ๐ฅ))) |
73 | 61, 72 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง Lim ๐ฅ) โ (โ
ยทo (๐ต
+o ๐ฅ)) =
((โ
ยทo ๐ต) +o (โ
ยทo ๐ฅ))) |
74 | 73 | ancoms 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 ๐ฅ)) |
78 | 76, 77 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ด = โ
โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = ((โ
ยทo ๐ต)
+o (โ
ยทo ๐ฅ))) |
79 | 75, 78 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (๐ด = โ
โ ((๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) โ (โ
ยทo
(๐ต +o ๐ฅ)) = ((โ
ยทo ๐ต)
+o (โ
ยทo ๐ฅ)))) |
80 | 74, 79 | syl5ibr 246 |
. . . . . . . . . 10
โข (๐ด = โ
โ ((Lim ๐ฅ โง ๐ต โ On) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)))) |
81 | 80 | expd 417 |
. . . . . . . . 9
โข (๐ด = โ
โ (Lim ๐ฅ โ (๐ต โ On โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
82 | 81 | com3r 87 |
. . . . . . . 8
โข (๐ต โ On โ (๐ด = โ
โ (Lim ๐ฅ โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
83 | 82 | imp 408 |
. . . . . . 7
โข ((๐ต โ On โง ๐ด = โ
) โ (Lim ๐ฅ โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)))) |
84 | 83 | a1dd 50 |
. . . . . 6
โข ((๐ต โ On โง ๐ด = โ
) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
85 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ ๐ต โ On) |
86 | 62 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ On โง ๐ต โ On) โ (๐ต +o ๐ฅ) โ On) |
87 | | onelon 6347 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ต +o ๐ฅ) โ On โง ๐ง โ (๐ต +o ๐ฅ)) โ ๐ง โ On) |
88 | 86, 87 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ ๐ง โ On) |
89 | | ontri1 6356 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ On โง ๐ง โ On) โ (๐ต โ ๐ง โ ยฌ ๐ง โ ๐ต)) |
90 | | oawordex 8509 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ On โง ๐ง โ On) โ (๐ต โ ๐ง โ โ๐ฃ โ On (๐ต +o ๐ฃ) = ๐ง)) |
91 | 89, 90 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ On โง ๐ง โ On) โ (ยฌ ๐ง โ ๐ต โ โ๐ฃ โ On (๐ต +o ๐ฃ) = ๐ง)) |
92 | 85, 88, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (ยฌ ๐ง โ ๐ต โ โ๐ฃ โ On (๐ต +o ๐ฃ) = ๐ง)) |
93 | | oaord 8499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฃ โ On โง ๐ฅ โ On โง ๐ต โ On) โ (๐ฃ โ ๐ฅ โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ))) |
94 | 93 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฃ โ On โง (๐ฅ โ On โง ๐ต โ On)) โ (๐ฃ โ ๐ฅ โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ))) |
95 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ต +o ๐ฃ) = ๐ง โ ((๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ) โ ๐ง โ (๐ต +o ๐ฅ))) |
96 | 94, 95 | sylan9bb 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ฃ โ On โง (๐ฅ โ On โง ๐ต โ On)) โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ฃ โ ๐ฅ โ ๐ง โ (๐ต +o ๐ฅ))) |
97 | | iba 529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ต +o ๐ฃ) = ๐ง โ (๐ฃ โ ๐ฅ โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
98 | 97 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ฃ โ On โง (๐ฅ โ On โง ๐ต โ On)) โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ฃ โ ๐ฅ โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
99 | 96, 98 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ฃ โ On โง (๐ฅ โ On โง ๐ต โ On)) โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ง โ (๐ต +o ๐ฅ) โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
100 | 99 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฃ โ On โง (๐ต +o ๐ฃ) = ๐ง) โง (๐ฅ โ On โง ๐ต โ On)) โ (๐ง โ (๐ต +o ๐ฅ) โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
101 | 100 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ง โ (๐ต +o ๐ฅ) โ (((๐ฃ โ On โง (๐ต +o ๐ฃ) = ๐ง) โง (๐ฅ โ On โง ๐ต โ On)) โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
102 | 101 | exp4c 434 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ง โ (๐ต +o ๐ฅ) โ (๐ฃ โ On โ ((๐ต +o ๐ฃ) = ๐ง โ ((๐ฅ โ On โง ๐ต โ On) โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))))) |
103 | 102 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ On โง ๐ต โ On) โ (๐ง โ (๐ต +o ๐ฅ) โ (๐ฃ โ On โ ((๐ต +o ๐ฃ) = ๐ง โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))))) |
104 | 103 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (๐ฃ โ On โ ((๐ต +o ๐ฃ) = ๐ง โ (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง)))) |
105 | 104 | reximdvai 3163 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (โ๐ฃ โ On (๐ต +o ๐ฃ) = ๐ง โ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
106 | 92, 105 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (ยฌ ๐ง โ ๐ต โ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
107 | 106 | orrd 862 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ On โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (๐ง โ ๐ต โจ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
108 | 61, 107 | sylanl1 679 |
. . . . . . . . . . . . . . . 16
โข (((Lim
๐ฅ โง ๐ต โ On) โง ๐ง โ (๐ต +o ๐ฅ)) โ (๐ง โ ๐ต โจ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
109 | 108 | adantlrl 719 |
. . . . . . . . . . . . . . 15
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ง โ (๐ต +o ๐ฅ)) โ (๐ง โ ๐ต โจ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง))) |
110 | 109 | adantlr 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 ๐ฅ)
โ (โ
โ ๐ด
โง โ
โ ๐ฅ))) |
113 | 112 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ด โ On โง ๐ฅ โ On) โ ((โ
โ ๐ด โง โ
โ ๐ฅ) โ โ
โ (๐ด
ยทo ๐ฅ))) |
114 | 111, 113 | sylan2i 607 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ด โ On โง ๐ฅ โ On) โ ((โ
โ ๐ด โง Lim ๐ฅ) โ โ
โ (๐ด ยทo ๐ฅ))) |
115 | 61, 114 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ On โง Lim ๐ฅ) โ ((โ
โ ๐ด โง Lim ๐ฅ) โ โ
โ (๐ด ยทo ๐ฅ))) |
116 | 115 | exp4b 432 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ด โ On โ (Lim ๐ฅ โ (โ
โ ๐ด โ (Lim ๐ฅ โ โ
โ (๐ด ยทo ๐ฅ))))) |
117 | 116 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (Lim
๐ฅ โ (๐ด โ On โ (Lim ๐ฅ โ (โ
โ ๐ด โ โ
โ (๐ด ยทo ๐ฅ))))) |
118 | 117 | pm2.43a 54 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (Lim
๐ฅ โ (๐ด โ On โ (โ
โ ๐ด โ โ
โ (๐ด ยทo ๐ฅ)))) |
119 | 118 | imp31 419 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((Lim
๐ฅ โง ๐ด โ On) โง โ
โ ๐ด) โ โ
โ (๐ด ยทo ๐ฅ)) |
120 | 119 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
โข (((Lim
๐ฅ โง ๐ด โ On) โง โ
โ ๐ด) โ (๐ง โ ๐ต โ โ
โ (๐ด ยทo ๐ฅ))) |
121 | 120 | adantlrr 720 |
. . . . . . . . . . . . . . . . . . 19
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ (๐ง โ ๐ต โ โ
โ (๐ด ยทo ๐ฅ))) |
122 | | omordi 8518 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ต โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ง โ ๐ต โ (๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต))) |
123 | 122 | ancom1s 652 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ง โ ๐ต โ (๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต))) |
124 | | onelss 6364 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด ยทo ๐ต) โ On โ ((๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต))) |
125 | 22 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด ยทo ๐ต) โ On โ ((๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
) โ (๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต))) |
126 | 124, 125 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด ยทo ๐ต) โ On โ ((๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
127 | 21, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ง) โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
129 | 123, 128 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ง โ ๐ต โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
130 | 129 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ (๐ง โ ๐ต โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
131 | 121, 130 | jcad 514 |
. . . . . . . . . . . . . . . . . 18
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ (๐ง โ ๐ต โ (โ
โ (๐ด ยทo ๐ฅ) โง (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
)))) |
132 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = โ
โ ((๐ด ยทo ๐ต) +o ๐ค) = ((๐ด ยทo ๐ต) +o โ
)) |
133 | 132 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ค = โ
โ ((๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o โ
))) |
134 | 133 | rspcev 3584 |
. . . . . . . . . . . . . . . . . 18
โข ((โ
โ (๐ด
ยทo ๐ฅ)
โง (๐ด
ยทo ๐ง)
โ ((๐ด
ยทo ๐ต)
+o โ
)) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค)) |
135 | 131, 134 | syl6 35 |
. . . . . . . . . . . . . . . . 17
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ (๐ง โ ๐ต โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
136 | 135 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ (๐ง โ ๐ต โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
137 | | omordi 8518 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ฃ โ ๐ฅ โ (๐ด ยทo ๐ฃ) โ (๐ด ยทo ๐ฅ))) |
138 | 61, 137 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((Lim
๐ฅ โง ๐ด โ On) โง โ
โ ๐ด) โ (๐ฃ โ ๐ฅ โ (๐ด ยทo ๐ฃ) โ (๐ด ยทo ๐ฅ))) |
139 | 138 | adantrd 493 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((Lim
๐ฅ โง ๐ด โ On) โง โ
โ ๐ด) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ด ยทo ๐ฃ) โ (๐ด ยทo ๐ฅ))) |
140 | 139 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
โข (((Lim
๐ฅ โง ๐ด โ On) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ด ยทo ๐ฃ) โ (๐ด ยทo ๐ฅ))) |
141 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = ๐ฃ โ (๐ต +o ๐ฆ) = (๐ต +o ๐ฃ)) |
142 | 141 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ = ๐ฃ โ (๐ด ยทo (๐ต +o ๐ฆ)) = (๐ด ยทo (๐ต +o ๐ฃ))) |
143 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = ๐ฃ โ (๐ด ยทo ๐ฆ) = (๐ด ยทo ๐ฃ)) |
144 | 143 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ = ๐ฃ โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) |
145 | 142, 144 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = ๐ฃ โ ((๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
146 | 145 | rspccv 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 ๐ง))) |
149 | 147, 148 | imbitrid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)) โ ((๐ต +o ๐ฃ) = ๐ง โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)) = (๐ด ยทo ๐ง))) |
150 | | eqimss2 4006 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)) = (๐ด ยทo ๐ง) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) |
151 | 149, 150 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)) โ ((๐ต +o ๐ฃ) = ๐ง โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
152 | 151 | imim2i 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฃ โ ๐ฅ โ (๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) โ (๐ฃ โ ๐ฅ โ ((๐ต +o ๐ฃ) = ๐ง โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))))) |
153 | 152 | impd 412 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฃ โ ๐ฅ โ (๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
154 | 146, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ฆ โ
๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
155 | 154 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
โข (((Lim
๐ฅ โง ๐ด โ On) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
156 | 140, 155 | jcad 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 ๐ฃ))) |
158 | 157 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
159 | 158 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด ยทo ๐ฃ) โ (๐ด ยทo ๐ฅ) โง (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค)) |
160 | 156, 159 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
โข (((Lim
๐ฅ โง ๐ด โ On) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ ((๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
161 | 160 | rexlimdvw 3158 |
. . . . . . . . . . . . . . . . 17
โข (((Lim
๐ฅ โง ๐ด โ On) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ (โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
162 | 161 | adantlrr 720 |
. . . . . . . . . . . . . . . 16
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ (โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
163 | 136, 162 | jaod 858 |
. . . . . . . . . . . . . . 15
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ ((๐ง โ ๐ต โจ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง)) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
164 | 163 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โง ๐ง โ (๐ต +o ๐ฅ)) โ ((๐ง โ ๐ต โจ โ๐ฃ โ On (๐ฃ โ ๐ฅ โง (๐ต +o ๐ฃ) = ๐ง)) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค))) |
165 | 110, 164 | mpd 15 |
. . . . . . . . . . . . 13
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โง ๐ง โ (๐ต +o ๐ฅ)) โ โ๐ค โ (๐ด ยทo ๐ฅ)(๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค)) |
166 | 165 | ralrimiva 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 ๐ค)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ โช ๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง) โ โช
๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค)) |
169 | | omordlim 8529 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ)) |
170 | 169 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ค โ (๐ด ยทo ๐ฅ) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ))) |
171 | 59, 170 | mpanr1 702 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ On โง Lim ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฅ) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ))) |
172 | 171 | ancoms 460 |
. . . . . . . . . . . . . . . . . 18
โข ((Lim
๐ฅ โง ๐ด โ On) โ (๐ค โ (๐ด ยทo ๐ฅ) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ))) |
173 | 172 | imp 408 |
. . . . . . . . . . . . . . . . 17
โข (((Lim
๐ฅ โง ๐ด โ On) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ)) |
174 | 173 | adantlrr 720 |
. . . . . . . . . . . . . . . 16
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ)) |
175 | 174 | adantlr 714 |
. . . . . . . . . . . . . . 15
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ)) |
176 | | oaordi 8498 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ โ On โง ๐ต โ On) โ (๐ฃ โ ๐ฅ โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ))) |
177 | 61, 176 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((Lim
๐ฅ โง ๐ต โ On) โ (๐ฃ โ ๐ฅ โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ))) |
178 | 177 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((Lim
๐ฅ โง ๐ต โ On) โง ๐ฃ โ ๐ฅ) โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ)) |
179 | 178 | adantlrl 719 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ฃ โ ๐ฅ) โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ)) |
180 | 179 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ (๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ))) |
181 | 180 | adantlr 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) |
184 | 182, 183 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((Lim
๐ฅ โง ๐ฃ โ ๐ฅ) โ ๐ฃ โ On) |
185 | | omcl 8487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ด โ On โง ๐ฃ โ On) โ (๐ด ยทo ๐ฃ) โ On) |
186 | 185 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฃ โ On โง ๐ด โ On) โ (๐ด ยทo ๐ฃ) โ On) |
187 | 186 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฃ โ On โง (๐ด โ On โง ๐ต โ On)) โ (๐ด ยทo ๐ฃ) โ On) |
188 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฃ โ On โง (๐ด โ On โง ๐ต โ On)) โ (๐ด ยทo ๐ต) โ On) |
189 | | oaordi 8498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ด ยทo ๐ฃ) โ On โง (๐ด ยทo ๐ต) โ On) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
190 | 187, 188,
189 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฃ โ On โง (๐ด โ On โง ๐ต โ On)) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
191 | 184, 190 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((Lim
๐ฅ โง ๐ฃ โ ๐ฅ) โง (๐ด โ On โง ๐ต โ On)) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
192 | 191 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
193 | 192 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
194 | 145 | rspccva 3583 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((โ๐ฆ โ
๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โง ๐ฃ โ ๐ฅ) โ (๐ด ยทo (๐ต +o ๐ฃ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ))) |
195 | 194 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((โ๐ฆ โ
๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โง ๐ฃ โ ๐ฅ) โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
196 | 195 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ ((๐ด ยทo ๐ต) +o ๐ค) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฃ)))) |
197 | 193, 196 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
198 | | oacl 8486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ต โ On โง ๐ฃ โ On) โ (๐ต +o ๐ฃ) โ On) |
199 | 198 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฃ โ On โง ๐ต โ On) โ (๐ต +o ๐ฃ) โ On) |
200 | | omcl 8487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ด โ On โง (๐ต +o ๐ฃ) โ On) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ On) |
201 | 199, 200 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ On โง (๐ฃ โ On โง ๐ต โ On)) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ On) |
202 | 201 | an12s 648 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฃ โ On โง (๐ด โ On โง ๐ต โ On)) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ On) |
203 | 184, 202 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((Lim
๐ฅ โง ๐ฃ โ ๐ฅ) โง (๐ด โ On โง ๐ต โ On)) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ On) |
204 | 203 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ฃ โ ๐ฅ) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ On) |
205 | | onelss 6364 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด ยทo (๐ต +o ๐ฃ)) โ On โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง ๐ฃ โ ๐ฅ) โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
207 | 206 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
208 | 197, 207 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
209 | 181, 208 | jcad 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 ๐ฃ))) |
211 | 210 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง = (๐ต +o ๐ฃ) โ (((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง) โ ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ)))) |
212 | 211 | rspcev 3584 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ต +o ๐ฃ) โ (๐ต +o ๐ฅ) โง ((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo (๐ต +o ๐ฃ))) โ โ๐ง โ (๐ต +o ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง)) |
213 | 209, 212 | syl6 35 |
. . . . . . . . . . . . . . . . 17
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ฃ โ ๐ฅ) โ (๐ค โ (๐ด ยทo ๐ฃ) โ โ๐ง โ (๐ต +o ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง))) |
214 | 213 | rexlimdva 3153 |
. . . . . . . . . . . . . . . 16
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โ (โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ) โ โ๐ง โ (๐ต +o ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง))) |
215 | 214 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ (โ๐ฃ โ ๐ฅ ๐ค โ (๐ด ยทo ๐ฃ) โ โ๐ง โ (๐ต +o ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง))) |
216 | 175, 215 | mpd 15 |
. . . . . . . . . . . . . 14
โข ((((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โง ๐ค โ (๐ด ยทo ๐ฅ)) โ โ๐ง โ (๐ต +o ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ (๐ด ยทo ๐ง)) |
217 | 216 | ralrimiva 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 ๐ง)) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . 12
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ))) โ โช ๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ โช
๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง)) |
220 | 219 | adantrl 715 |
. . . . . . . . . . 11
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ โช ๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค) โ โช
๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง)) |
221 | 168, 220 | eqssd 3966 |
. . . . . . . . . 10
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ โช ๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง) = โช ๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค)) |
222 | | oalimcl 8512 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ Lim (๐ต +o ๐ฅ)) |
223 | 59, 222 | mpanr1 702 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ On โง Lim ๐ฅ) โ Lim (๐ต +o ๐ฅ)) |
224 | 223 | ancoms 460 |
. . . . . . . . . . . . . 14
โข ((Lim
๐ฅ โง ๐ต โ On) โ Lim (๐ต +o ๐ฅ)) |
225 | 224 | anim2i 618 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง (Lim ๐ฅ โง ๐ต โ On)) โ (๐ด โ On โง Lim (๐ต +o ๐ฅ))) |
226 | 225 | an12s 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 ๐ง)) |
229 | 227, 228 | mpanr1 702 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง Lim (๐ต +o ๐ฅ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = โช
๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง)) |
230 | 226, 229 | syl 17 |
. . . . . . . . . . 11
โข ((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = โช
๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง)) |
231 | 230 | adantr 482 |
. . . . . . . . . 10
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ (๐ด ยทo (๐ต +o ๐ฅ)) = โช
๐ง โ (๐ต +o ๐ฅ)(๐ด ยทo ๐ง)) |
232 | 21 | ad2antlr 726 |
. . . . . . . . . . . 12
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ (๐ด ยทo ๐ต) โ On) |
233 | 59 | jctl 525 |
. . . . . . . . . . . . . . . 16
โข (Lim
๐ฅ โ (๐ฅ โ V โง Lim ๐ฅ)) |
234 | 233 | anim1ci 617 |
. . . . . . . . . . . . . . 15
โข ((Lim
๐ฅ โง ๐ด โ On) โ (๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ))) |
235 | | omlimcl 8530 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ด) โ Lim (๐ด ยทo ๐ฅ)) |
236 | 234, 235 | sylan 581 |
. . . . . . . . . . . . . 14
โข (((Lim
๐ฅ โง ๐ด โ On) โง โ
โ ๐ด) โ Lim (๐ด ยทo ๐ฅ)) |
237 | 236 | adantlrr 720 |
. . . . . . . . . . . . 13
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ Lim (๐ด ยทo ๐ฅ)) |
238 | | ovex 7395 |
. . . . . . . . . . . . 13
โข (๐ด ยทo ๐ฅ) โ V |
239 | 237, 238 | jctil 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 ๐ค)) |
241 | 232, 239,
240 | syl2anc 585 |
. . . . . . . . . . 11
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง โ
โ ๐ด) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = โช
๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค)) |
242 | 241 | adantrr 716 |
. . . . . . . . . 10
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)) = โช
๐ค โ (๐ด ยทo ๐ฅ)((๐ด ยทo ๐ต) +o ๐ค)) |
243 | 221, 231,
242 | 3eqtr4d 2787 |
. . . . . . . . 9
โข (((Lim
๐ฅ โง (๐ด โ On โง ๐ต โ On)) โง (โ
โ ๐ด โง โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)))) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))) |
244 | 243 | exp43 438 |
. . . . . . . 8
โข (Lim
๐ฅ โ ((๐ด โ On โง ๐ต โ On) โ (โ
โ ๐ด โ
(โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)))))) |
245 | 244 | com3l 89 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (โ
โ ๐ด โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ)))))) |
246 | 245 | imp 408 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
247 | 84, 246 | oe0lem 8464 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
248 | 247 | com12 32 |
. . . 4
โข (Lim
๐ฅ โ ((๐ด โ On โง ๐ต โ On) โ
(โ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต +o ๐ฆ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฆ)) โ (๐ด ยทo (๐ต +o ๐ฅ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ฅ))))) |
249 | 5, 10, 15, 20, 30, 58, 248 | tfinds3 7806 |
. . 3
โข (๐ถ โ On โ ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo (๐ต +o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ)))) |
250 | 249 | expdcom 416 |
. 2
โข (๐ด โ On โ (๐ต โ On โ (๐ถ โ On โ (๐ด ยทo (๐ต +o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))))) |
251 | 250 | 3imp 1112 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด ยทo (๐ต +o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |