Step | Hyp | Ref
| Expression |
1 | | limelon 6385 |
. . . 4
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ ๐ต โ On) |
2 | | omcl 8486 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
3 | | eloni 6331 |
. . . . 5
โข ((๐ด ยทo ๐ต) โ On โ Ord (๐ด ยทo ๐ต)) |
4 | 2, 3 | syl 17 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ Ord (๐ด ยทo ๐ต)) |
5 | 1, 4 | sylan2 594 |
. . 3
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ Ord (๐ด ยทo ๐ต)) |
6 | 5 | adantr 482 |
. 2
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ Ord (๐ด ยทo ๐ต)) |
7 | | 0ellim 6384 |
. . . . . . . 8
โข (Lim
๐ต โ โ
โ
๐ต) |
8 | | n0i 4297 |
. . . . . . . 8
โข (โ
โ ๐ต โ ยฌ ๐ต = โ
) |
9 | 7, 8 | syl 17 |
. . . . . . 7
โข (Lim
๐ต โ ยฌ ๐ต = โ
) |
10 | | n0i 4297 |
. . . . . . 7
โข (โ
โ ๐ด โ ยฌ ๐ด = โ
) |
11 | 9, 10 | anim12ci 615 |
. . . . . 6
โข ((Lim
๐ต โง โ
โ
๐ด) โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
)) |
12 | 11 | adantll 713 |
. . . . 5
โข (((๐ต โ ๐ถ โง Lim ๐ต) โง โ
โ ๐ด) โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
)) |
13 | 12 | adantll 713 |
. . . 4
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
)) |
14 | | om00 8526 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
))) |
15 | 14 | notbid 318 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (ยฌ (๐ด ยทo ๐ต) = โ
โ ยฌ (๐ด = โ
โจ ๐ต = โ
))) |
16 | | ioran 983 |
. . . . . . 7
โข (ยฌ
(๐ด = โ
โจ ๐ต = โ
) โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
)) |
17 | 15, 16 | bitrdi 287 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (ยฌ (๐ด ยทo ๐ต) = โ
โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
))) |
18 | 1, 17 | sylan2 594 |
. . . . 5
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ (ยฌ (๐ด ยทo ๐ต) = โ
โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
))) |
19 | 18 | adantr 482 |
. . . 4
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (ยฌ (๐ด ยทo ๐ต) = โ
โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
))) |
20 | 13, 19 | mpbird 257 |
. . 3
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ยฌ (๐ด ยทo ๐ต) = โ
) |
21 | | vex 3451 |
. . . . . . . . . . 11
โข ๐ฆ โ V |
22 | 21 | sucid 6403 |
. . . . . . . . . 10
โข ๐ฆ โ suc ๐ฆ |
23 | | omlim 8483 |
. . . . . . . . . . 11
โข ((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โ (๐ด ยทo ๐ต) = โช
๐ฅ โ ๐ต (๐ด ยทo ๐ฅ)) |
24 | | eqeq1 2737 |
. . . . . . . . . . . 12
โข ((๐ด ยทo ๐ต) = suc ๐ฆ โ ((๐ด ยทo ๐ต) = โช
๐ฅ โ ๐ต (๐ด ยทo ๐ฅ) โ suc ๐ฆ = โช ๐ฅ โ ๐ต (๐ด ยทo ๐ฅ))) |
25 | 24 | biimpac 480 |
. . . . . . . . . . 11
โข (((๐ด ยทo ๐ต) = โช ๐ฅ โ ๐ต (๐ด ยทo ๐ฅ) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ suc ๐ฆ = โช ๐ฅ โ ๐ต (๐ด ยทo ๐ฅ)) |
26 | 23, 25 | sylan 581 |
. . . . . . . . . 10
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ suc ๐ฆ = โช ๐ฅ โ ๐ต (๐ด ยทo ๐ฅ)) |
27 | 22, 26 | eleqtrid 2840 |
. . . . . . . . 9
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ ๐ฆ โ โช
๐ฅ โ ๐ต (๐ด ยทo ๐ฅ)) |
28 | | eliun 4962 |
. . . . . . . . 9
โข (๐ฆ โ โช ๐ฅ โ ๐ต (๐ด ยทo ๐ฅ) โ โ๐ฅ โ ๐ต ๐ฆ โ (๐ด ยทo ๐ฅ)) |
29 | 27, 28 | sylib 217 |
. . . . . . . 8
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ โ๐ฅ โ ๐ต ๐ฆ โ (๐ด ยทo ๐ฅ)) |
30 | 29 | adantlr 714 |
. . . . . . 7
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ โ๐ฅ โ ๐ต ๐ฆ โ (๐ด ยทo ๐ฅ)) |
31 | | onelon 6346 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
32 | 1, 31 | sylan 581 |
. . . . . . . . . . . 12
โข (((๐ต โ ๐ถ โง Lim ๐ต) โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
33 | | onnbtwn 6415 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ On โ ยฌ (๐ฅ โ ๐ต โง ๐ต โ suc ๐ฅ)) |
34 | | imnan 401 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ ๐ต โ ยฌ ๐ต โ suc ๐ฅ) โ ยฌ (๐ฅ โ ๐ต โง ๐ต โ suc ๐ฅ)) |
35 | 33, 34 | sylibr 233 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ On โ (๐ฅ โ ๐ต โ ยฌ ๐ต โ suc ๐ฅ)) |
36 | 35 | com12 32 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ต โ (๐ฅ โ On โ ยฌ ๐ต โ suc ๐ฅ)) |
37 | 36 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ต โ ๐ถ โง Lim ๐ต) โง ๐ฅ โ ๐ต) โ (๐ฅ โ On โ ยฌ ๐ต โ suc ๐ฅ)) |
38 | 32, 37 | mpd 15 |
. . . . . . . . . . 11
โข (((๐ต โ ๐ถ โง Lim ๐ต) โง ๐ฅ โ ๐ต) โ ยฌ ๐ต โ suc ๐ฅ) |
39 | 38 | ad5ant24 760 |
. . . . . . . . . 10
โข
(((((๐ด โ On
โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ฅ โ ๐ต) โง ๐ฆ โ (๐ด ยทo ๐ฅ)) โ ยฌ ๐ต โ suc ๐ฅ) |
40 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ ๐ต โ On) |
41 | 40, 31 | jca 513 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ (๐ต โ On โง ๐ฅ โ On)) |
42 | 1, 41 | sylan 581 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ ๐ถ โง Lim ๐ต) โง ๐ฅ โ ๐ต) โ (๐ต โ On โง ๐ฅ โ On)) |
43 | 42 | anim2i 618 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ((๐ต โ ๐ถ โง Lim ๐ต) โง ๐ฅ โ ๐ต)) โ (๐ด โ On โง (๐ต โ On โง ๐ฅ โ On))) |
44 | 43 | anassrs 469 |
. . . . . . . . . . . . 13
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง ๐ฅ โ ๐ต) โ (๐ด โ On โง (๐ต โ On โง ๐ฅ โ On))) |
45 | | omcl 8486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ด ยทo ๐ฅ) โ On) |
46 | | eloni 6331 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด ยทo ๐ฅ) โ On โ Ord (๐ด ยทo ๐ฅ)) |
47 | | ordsucelsuc 7761 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (Ord
(๐ด ยทo
๐ฅ) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ suc (๐ด ยทo ๐ฅ))) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด ยทo ๐ฅ) โ On โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ suc (๐ด ยทo ๐ฅ))) |
49 | | oa1suc 8481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด ยทo ๐ฅ) โ On โ ((๐ด ยทo ๐ฅ) +o 1o) =
suc (๐ด ยทo
๐ฅ)) |
50 | 49 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด ยทo ๐ฅ) โ On โ (suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o 1o) โ suc
๐ฆ โ suc (๐ด ยทo ๐ฅ))) |
51 | 48, 50 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด ยทo ๐ฅ) โ On โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o
1o))) |
52 | 45, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o
1o))) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o
1o))) |
54 | | eloni 6331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ด โ On โ Ord ๐ด) |
55 | | ordgt0ge1 8443 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (Ord
๐ด โ (โ
โ
๐ด โ 1o
โ ๐ด)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ด โ On โ (โ
โ ๐ด โ
1o โ ๐ด)) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ On โง ๐ฅ โ On) โ (โ
โ ๐ด โ
1o โ ๐ด)) |
58 | | 1on 8428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
1o โ On |
59 | | oaword 8500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((1o โ On โง ๐ด โ On โง (๐ด ยทo ๐ฅ) โ On) โ (1o โ
๐ด โ ((๐ด ยทo ๐ฅ) +o 1o)
โ ((๐ด
ยทo ๐ฅ)
+o ๐ด))) |
60 | 58, 59 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ On โง (๐ด ยทo ๐ฅ) โ On) โ
(1o โ ๐ด
โ ((๐ด
ยทo ๐ฅ)
+o 1o) โ ((๐ด ยทo ๐ฅ) +o ๐ด))) |
61 | 45, 60 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ On โง ๐ฅ โ On) โ
(1o โ ๐ด
โ ((๐ด
ยทo ๐ฅ)
+o 1o) โ ((๐ด ยทo ๐ฅ) +o ๐ด))) |
62 | 57, 61 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ On โง ๐ฅ โ On) โ (โ
โ ๐ด โ ((๐ด ยทo ๐ฅ) +o 1o)
โ ((๐ด
ยทo ๐ฅ)
+o ๐ด))) |
63 | 62 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ฅ) +o 1o)
โ ((๐ด
ยทo ๐ฅ)
+o ๐ด)) |
64 | | omsuc 8476 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ด ยทo suc ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ด)) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (๐ด ยทo suc ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ด)) |
66 | 63, 65 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ฅ) +o 1o)
โ (๐ด
ยทo suc ๐ฅ)) |
67 | 66 | sseld 3947 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o 1o) โ suc
๐ฆ โ (๐ด ยทo suc ๐ฅ))) |
68 | 53, 67 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ suc ๐ฆ โ (๐ด ยทo suc ๐ฅ))) |
69 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด ยทo ๐ต) = suc ๐ฆ โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ suc ๐ฆ โ (๐ด ยทo suc ๐ฅ))) |
70 | 69 | biimprd 248 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด ยทo ๐ต) = suc ๐ฆ โ (suc ๐ฆ โ (๐ด ยทo suc ๐ฅ) โ (๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ))) |
71 | 68, 70 | syl9 77 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ (๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ)))) |
72 | 71 | com23 86 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ (๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ)))) |
73 | 72 | adantlrl 719 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง (๐ต โ On โง ๐ฅ โ On)) โง โ
โ ๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ (๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ)))) |
74 | | onsucb 7756 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ On โ suc ๐ฅ โ On) |
75 | | omord 8519 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ On โง suc ๐ฅ โ On โง ๐ด โ On) โ ((๐ต โ suc ๐ฅ โง โ
โ ๐ด) โ (๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ))) |
76 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ suc ๐ฅ โง โ
โ ๐ด) โ ๐ต โ suc ๐ฅ) |
77 | 75, 76 | syl6bir 254 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ On โง suc ๐ฅ โ On โง ๐ด โ On) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ ๐ต โ suc ๐ฅ)) |
78 | 74, 77 | syl3an2b 1405 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ On โง ๐ฅ โ On โง ๐ด โ On) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ ๐ต โ suc ๐ฅ)) |
79 | 78 | 3comr 1126 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ On โง ๐ต โ On โง ๐ฅ โ On) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ ๐ต โ suc ๐ฅ)) |
80 | 79 | 3expb 1121 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ On โง (๐ต โ On โง ๐ฅ โ On)) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ ๐ต โ suc ๐ฅ)) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง (๐ต โ On โง ๐ฅ โ On)) โง โ
โ ๐ด) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo suc ๐ฅ) โ ๐ต โ suc ๐ฅ)) |
82 | 73, 81 | syl6d 75 |
. . . . . . . . . . . . 13
โข (((๐ด โ On โง (๐ต โ On โง ๐ฅ โ On)) โง โ
โ ๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ ๐ต โ suc ๐ฅ))) |
83 | 44, 82 | sylan 581 |
. . . . . . . . . . . 12
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง ๐ฅ โ ๐ต) โง โ
โ ๐ด) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ ๐ต โ suc ๐ฅ))) |
84 | 83 | an32s 651 |
. . . . . . . . . . 11
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ฅ โ ๐ต) โ (๐ฆ โ (๐ด ยทo ๐ฅ) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ ๐ต โ suc ๐ฅ))) |
85 | 84 | imp 408 |
. . . . . . . . . 10
โข
(((((๐ด โ On
โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ฅ โ ๐ต) โง ๐ฆ โ (๐ด ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) = suc ๐ฆ โ ๐ต โ suc ๐ฅ)) |
86 | 39, 85 | mtod 197 |
. . . . . . . . 9
โข
(((((๐ด โ On
โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ฅ โ ๐ต) โง ๐ฆ โ (๐ด ยทo ๐ฅ)) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ) |
87 | 86 | rexlimdva2 3151 |
. . . . . . . 8
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (โ๐ฅ โ ๐ต ๐ฆ โ (๐ด ยทo ๐ฅ) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ)) |
88 | 87 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ (โ๐ฅ โ ๐ต ๐ฆ โ (๐ด ยทo ๐ฅ) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ)) |
89 | 30, 88 | mpd 15 |
. . . . . 6
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง (๐ด ยทo ๐ต) = suc ๐ฆ) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ) |
90 | 89 | pm2.01da 798 |
. . . . 5
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ) |
91 | 90 | adantr 482 |
. . . 4
โข ((((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โง ๐ฆ โ On) โ ยฌ (๐ด ยทo ๐ต) = suc ๐ฆ) |
92 | 91 | nrexdv 3143 |
. . 3
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ยฌ โ๐ฆ โ On (๐ด ยทo ๐ต) = suc ๐ฆ) |
93 | | ioran 983 |
. . 3
โข (ยฌ
((๐ด ยทo
๐ต) = โ
โจ
โ๐ฆ โ On (๐ด ยทo ๐ต) = suc ๐ฆ) โ (ยฌ (๐ด ยทo ๐ต) = โ
โง ยฌ โ๐ฆ โ On (๐ด ยทo ๐ต) = suc ๐ฆ)) |
94 | 20, 92, 93 | sylanbrc 584 |
. 2
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ ยฌ ((๐ด ยทo ๐ต) = โ
โจ โ๐ฆ โ On (๐ด ยทo ๐ต) = suc ๐ฆ)) |
95 | | dflim3 7787 |
. 2
โข (Lim
(๐ด ยทo
๐ต) โ (Ord (๐ด ยทo ๐ต) โง ยฌ ((๐ด ยทo ๐ต) = โ
โจ โ๐ฆ โ On (๐ด ยทo ๐ต) = suc ๐ฆ))) |
96 | 6, 94, 95 | sylanbrc 584 |
1
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ Lim (๐ด ยทo ๐ต)) |