Step | Hyp | Ref
| Expression |
1 | | eloni 6328 |
. . . . . 6
โข (๐ด โ On โ Ord ๐ด) |
2 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ Ord ๐ด) |
3 | | ne0i 4295 |
. . . . . 6
โข (โ
โ ๐ด โ ๐ด โ โ
) |
4 | 3 | adantl 483 |
. . . . 5
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ๐ด โ โ
) |
5 | | id 22 |
. . . . 5
โข (๐ด = โช
๐ด โ ๐ด = โช ๐ด) |
6 | | df-lim 6323 |
. . . . . 6
โข (Lim
๐ด โ (Ord ๐ด โง ๐ด โ โ
โง ๐ด = โช ๐ด)) |
7 | 6 | biimpri 227 |
. . . . 5
โข ((Ord
๐ด โง ๐ด โ โ
โง ๐ด = โช ๐ด) โ Lim ๐ด) |
8 | 2, 4, 5, 7 | syl2an3an 1423 |
. . . 4
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = โช ๐ด) โ Lim ๐ด) |
9 | 8 | ex 414 |
. . 3
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด = โช ๐ด โ Lim ๐ด)) |
10 | | limelon 6382 |
. . . . . 6
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ ๐ต โ On) |
11 | 10 | ad3antlr 730 |
. . . . 5
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง Lim ๐ด) โ ๐ต โ On) |
12 | | simpll 766 |
. . . . . 6
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ๐ด โ On) |
13 | 12 | anim1i 616 |
. . . . 5
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง Lim ๐ด) โ (๐ด โ On โง Lim ๐ด)) |
14 | | 0ellim 6381 |
. . . . . . 7
โข (Lim
๐ต โ โ
โ
๐ต) |
15 | 14 | adantl 483 |
. . . . . 6
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ โ
โ ๐ต) |
16 | 15 | ad3antlr 730 |
. . . . 5
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง Lim ๐ด) โ โ
โ ๐ต) |
17 | | omlimcl 8526 |
. . . . 5
โข (((๐ต โ On โง (๐ด โ On โง Lim ๐ด)) โง โ
โ ๐ต) โ Lim (๐ต ยทo ๐ด)) |
18 | 11, 13, 16, 17 | syl21anc 837 |
. . . 4
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง Lim ๐ด) โ Lim (๐ต ยทo ๐ด)) |
19 | 18 | ex 414 |
. . 3
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (Lim ๐ด โ Lim (๐ต ยทo ๐ด))) |
20 | 9, 19 | syld 47 |
. 2
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด = โช ๐ด โ Lim (๐ต ยทo ๐ด))) |
21 | | onuni 7724 |
. . . . . . . . 9
โข (๐ด โ On โ โช ๐ด
โ On) |
22 | 21, 10 | anim12ci 615 |
. . . . . . . 8
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ (๐ต โ On โง โช ๐ด
โ On)) |
23 | | omcl 8483 |
. . . . . . . 8
โข ((๐ต โ On โง โช ๐ด
โ On) โ (๐ต
ยทo โช ๐ด) โ On) |
24 | 22, 23 | syl 17 |
. . . . . . 7
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ (๐ต ยทo โช ๐ด)
โ On) |
25 | | simpr 486 |
. . . . . . 7
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ (๐ต โ ๐ถ โง Lim ๐ต)) |
26 | 24, 25 | jca 513 |
. . . . . 6
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ ((๐ต ยทo โช ๐ด)
โ On โง (๐ต โ
๐ถ โง Lim ๐ต))) |
27 | 26 | ad2antrr 725 |
. . . . 5
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ ((๐ต ยทo โช ๐ด)
โ On โง (๐ต โ
๐ถ โง Lim ๐ต))) |
28 | | oalimcl 8508 |
. . . . 5
โข (((๐ต ยทo โช ๐ด)
โ On โง (๐ต โ
๐ถ โง Lim ๐ต)) โ Lim ((๐ต ยทo โช ๐ด)
+o ๐ต)) |
29 | 27, 28 | syl 17 |
. . . 4
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ Lim ((๐ต ยทo โช ๐ด)
+o ๐ต)) |
30 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ ๐ด = suc โช ๐ด) |
31 | 30 | oveq2d 7374 |
. . . . . 6
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ (๐ต ยทo ๐ด) = (๐ต ยทo suc โช ๐ด)) |
32 | 22 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ (๐ต โ On โง โช ๐ด
โ On)) |
33 | | omsuc 8473 |
. . . . . . 7
โข ((๐ต โ On โง โช ๐ด
โ On) โ (๐ต
ยทo suc โช ๐ด) = ((๐ต ยทo โช ๐ด)
+o ๐ต)) |
34 | 32, 33 | syl 17 |
. . . . . 6
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ (๐ต ยทo suc โช ๐ด) =
((๐ต ยทo
โช ๐ด) +o ๐ต)) |
35 | 31, 34 | eqtrd 2773 |
. . . . 5
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ (๐ต ยทo ๐ด) = ((๐ต ยทo โช ๐ด)
+o ๐ต)) |
36 | | limeq 6330 |
. . . . 5
โข ((๐ต ยทo ๐ด) = ((๐ต ยทo โช ๐ด)
+o ๐ต) โ
(Lim (๐ต
ยทo ๐ด)
โ Lim ((๐ต
ยทo โช ๐ด) +o ๐ต))) |
37 | 35, 36 | syl 17 |
. . . 4
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ (Lim (๐ต ยทo ๐ด) โ Lim ((๐ต ยทo โช ๐ด)
+o ๐ต))) |
38 | 29, 37 | mpbird 257 |
. . 3
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ด = suc โช ๐ด) โ Lim (๐ต ยทo ๐ด)) |
39 | 38 | ex 414 |
. 2
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด = suc โช ๐ด โ Lim (๐ต ยทo ๐ด))) |
40 | | orduniorsuc 7766 |
. . 3
โข (Ord
๐ด โ (๐ด = โช ๐ด โจ ๐ด = suc โช ๐ด)) |
41 | 2, 40 | syl 17 |
. 2
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด = โช ๐ด โจ ๐ด = suc โช ๐ด)) |
42 | 20, 39, 41 | mpjaod 859 |
1
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ Lim (๐ต ยทo ๐ด)) |