Step | Hyp | Ref
| Expression |
1 | | limord 6382 |
. . . . 5
โข (Lim
๐ด โ Ord ๐ด) |
2 | | ordeleqon 7721 |
. . . . . . 7
โข (Ord
๐ด โ (๐ด โ On โจ ๐ด = On)) |
3 | 2 | biimpi 215 |
. . . . . 6
โข (Ord
๐ด โ (๐ด โ On โจ ๐ด = On)) |
4 | 3 | orcomd 870 |
. . . . 5
โข (Ord
๐ด โ (๐ด = On โจ ๐ด โ On)) |
5 | 1, 4 | syl 17 |
. . . 4
โข (Lim
๐ด โ (๐ด = On โจ ๐ด โ On)) |
6 | 5 | pm4.71ri 562 |
. . 3
โข (Lim
๐ด โ ((๐ด = On โจ ๐ด โ On) โง Lim ๐ด)) |
7 | | andir 1008 |
. . 3
โข (((๐ด = On โจ ๐ด โ On) โง Lim ๐ด) โ ((๐ด = On โง Lim ๐ด) โจ (๐ด โ On โง Lim ๐ด))) |
8 | 6, 7 | bitri 275 |
. 2
โข (Lim
๐ด โ ((๐ด = On โง Lim ๐ด) โจ (๐ด โ On โง Lim ๐ด))) |
9 | | limon 7776 |
. . . . 5
โข Lim
On |
10 | | limeq 6334 |
. . . . 5
โข (๐ด = On โ (Lim ๐ด โ Lim
On)) |
11 | 9, 10 | mpbiri 258 |
. . . 4
โข (๐ด = On โ Lim ๐ด) |
12 | 11 | pm4.71i 561 |
. . 3
โข (๐ด = On โ (๐ด = On โง Lim ๐ด)) |
13 | 12 | orbi1i 913 |
. 2
โข ((๐ด = On โจ (๐ด โ On โง Lim ๐ด)) โ ((๐ด = On โง Lim ๐ด) โจ (๐ด โ On โง Lim ๐ด))) |
14 | | simpl 484 |
. . . . . 6
โข ((๐ด โ On โง Lim ๐ด) โ ๐ด โ On) |
15 | | omelon 9589 |
. . . . . . . 8
โข ฯ
โ On |
16 | 15 | a1i 11 |
. . . . . . 7
โข (๐ด โ On โ ฯ โ
On) |
17 | | id 22 |
. . . . . . 7
โข (๐ด โ On โ ๐ด โ On) |
18 | | peano1 7830 |
. . . . . . . . 9
โข โ
โ ฯ |
19 | 18 | ne0ii 4302 |
. . . . . . . 8
โข ฯ
โ โ
|
20 | 19 | a1i 11 |
. . . . . . 7
โข (๐ด โ On โ ฯ โ
โ
) |
21 | 16, 17, 20 | 3jca 1129 |
. . . . . 6
โข (๐ด โ On โ (ฯ
โ On โง ๐ด โ On
โง ฯ โ โ
)) |
22 | | omeulem1 8534 |
. . . . . 6
โข ((ฯ
โ On โง ๐ด โ On
โง ฯ โ โ
) โ โ๐ฅ โ On โ๐ฆ โ ฯ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) |
23 | 14, 21, 22 | 3syl 18 |
. . . . 5
โข ((๐ด โ On โง Lim ๐ด) โ โ๐ฅ โ On โ๐ฆ โ ฯ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) |
24 | | limeq 6334 |
. . . . . . . . . . . . . . . 16
โข
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ด โ (Lim ((ฯ ยทo
๐ฅ) +o ๐ฆ) โ Lim ๐ด)) |
25 | 24 | biimprd 248 |
. . . . . . . . . . . . . . 15
โข
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ด โ (Lim ๐ด โ Lim ((ฯ ยทo
๐ฅ) +o ๐ฆ))) |
26 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
๐ฆ โ
ฯ) |
27 | | nnlim 7821 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ ฯ โ ยฌ Lim
๐ฆ) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
ยฌ Lim ๐ฆ) |
29 | | on0eln0 6378 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ โ On โ (โ
โ ๐ฅ โ ๐ฅ โ โ
)) |
30 | 29 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ โ On โ (๐ฅ โ โ
โ โ
โ ๐ฅ)) |
31 | 30 | necon1bd 2962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ โ On โ (ยฌ โ
โ ๐ฅ โ ๐ฅ = โ
)) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (ยฌ
โ
โ ๐ฅ โ
๐ฅ =
โ
)) |
33 | 32 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
๐ฅ =
โ
) |
34 | 33, 26 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
(๐ฅ = โ
โง ๐ฆ โ
ฯ)) |
35 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ ๐ฅ = โ
) |
36 | 35 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ (ฯ
ยทo ๐ฅ) =
(ฯ ยทo โ
)) |
37 | | om0 8468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (ฯ
โ On โ (ฯ ยทo โ
) =
โ
) |
38 | 15, 37 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ (ฯ
ยทo โ
) = โ
) |
39 | 36, 38 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ (ฯ
ยทo ๐ฅ) =
โ
) |
40 | 39 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ
((ฯ ยทo ๐ฅ) +o ๐ฆ) = (โ
+o ๐ฆ)) |
41 | | nna0r 8561 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ ฯ โ (โ
+o ๐ฆ) = ๐ฆ) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ (โ
+o ๐ฆ) = ๐ฆ) |
43 | 40, 42 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ = โ
โง ๐ฆ โ ฯ) โ
((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ฆ) |
44 | | limeq 6334 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ฆ โ (Lim ((ฯ ยทo
๐ฅ) +o ๐ฆ) โ Lim ๐ฆ)) |
45 | 34, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
(Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ) โ Lim ๐ฆ)) |
46 | 28, 45 | mtbird 325 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
โ
โ ๐ฅ) โ
ยฌ Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ)) |
47 | 46 | ex 414 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (ยฌ
โ
โ ๐ฅ โ
ยฌ Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ))) |
48 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((ฯ
ยทo ๐ฅ)
+o โช ๐ฆ) โ V |
49 | | nlimsucg 7783 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ ยทo ๐ฅ) +o โช
๐ฆ) โ V โ ยฌ
Lim suc ((ฯ ยทo ๐ฅ) +o โช
๐ฆ)) |
50 | 48, 49 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ ยฌ
Lim suc ((ฯ ยทo ๐ฅ) +o โช
๐ฆ)) |
51 | | nnord 7815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฆ โ ฯ โ Ord ๐ฆ) |
52 | | orduniorsuc 7770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (Ord
๐ฆ โ (๐ฆ = โช
๐ฆ โจ ๐ฆ = suc โช ๐ฆ)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฆ โ ฯ โ (๐ฆ = โช
๐ฆ โจ ๐ฆ = suc โช ๐ฆ)) |
54 | | 3ianor 1108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (ยฌ
(Ord ๐ฆ โง ๐ฆ โ โ
โง ๐ฆ = โช
๐ฆ) โ (ยฌ Ord ๐ฆ โจ ยฌ ๐ฆ โ โ
โจ ยฌ ๐ฆ = โช ๐ฆ)) |
55 | | df-lim 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (Lim
๐ฆ โ (Ord ๐ฆ โง ๐ฆ โ โ
โง ๐ฆ = โช ๐ฆ)) |
56 | 54, 55 | xchnxbir 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (ยฌ
Lim ๐ฆ โ (ยฌ Ord
๐ฆ โจ ยฌ ๐ฆ โ โ
โจ ยฌ ๐ฆ = โช
๐ฆ)) |
57 | 27, 56 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฆ โ ฯ โ (ยฌ
Ord ๐ฆ โจ ยฌ ๐ฆ โ โ
โจ ยฌ ๐ฆ = โช
๐ฆ)) |
58 | 51 | pm2.24d 151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฆ โ ฯ โ (ยฌ
Ord ๐ฆ โ (๐ฆ = โช
๐ฆ โ ๐ฆ = โ
))) |
59 | | nne 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (ยฌ
๐ฆ โ โ
โ ๐ฆ = โ
) |
60 | 59 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (ยฌ
๐ฆ โ โ
โ ๐ฆ = โ
) |
61 | 60 | a1i13 27 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฆ โ ฯ โ (ยฌ
๐ฆ โ โ
โ
(๐ฆ = โช ๐ฆ
โ ๐ฆ =
โ
))) |
62 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (ยฌ
๐ฆ = โช ๐ฆ
โ (๐ฆ = โช ๐ฆ
โ ๐ฆ =
โ
)) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฆ โ ฯ โ (ยฌ
๐ฆ = โช ๐ฆ
โ (๐ฆ = โช ๐ฆ
โ ๐ฆ =
โ
))) |
64 | 58, 61, 63 | 3jaod 1429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฆ โ ฯ โ ((ยฌ
Ord ๐ฆ โจ ยฌ ๐ฆ โ โ
โจ ยฌ ๐ฆ = โช
๐ฆ) โ (๐ฆ = โช
๐ฆ โ ๐ฆ = โ
))) |
65 | 57, 64 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฆ โ ฯ โ (๐ฆ = โช
๐ฆ โ ๐ฆ = โ
)) |
66 | 65 | orim1d 965 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฆ โ ฯ โ ((๐ฆ = โช
๐ฆ โจ ๐ฆ = suc โช ๐ฆ) โ (๐ฆ = โ
โจ ๐ฆ = suc โช ๐ฆ))) |
67 | 53, 66 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ โ ฯ โ (๐ฆ = โ
โจ ๐ฆ = suc โช ๐ฆ)) |
68 | 67 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ ฯ โ (ยฌ
๐ฆ = โ
โ ๐ฆ = suc โช ๐ฆ)) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (ยฌ
๐ฆ = โ
โ ๐ฆ = suc โช ๐ฆ)) |
70 | 69 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ ๐ฆ = suc โช ๐ฆ) |
71 | 70 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ
((ฯ ยทo ๐ฅ) +o ๐ฆ) = ((ฯ ยทo ๐ฅ) +o suc โช ๐ฆ)) |
72 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ ๐ฅ โ On) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ ๐ฅ โ On) |
74 | | omcl 8487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((ฯ
โ On โง ๐ฅ โ
On) โ (ฯ ยทo ๐ฅ) โ On) |
75 | 15, 73, 74 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ
(ฯ ยทo ๐ฅ) โ On) |
76 | | nnon 7813 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ โ ฯ โ ๐ฆ โ On) |
77 | | onuni 7728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ โ On โ โช ๐ฆ
โ On) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ ฯ โ โช ๐ฆ
โ On) |
79 | 78 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ โช ๐ฆ
โ On) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ โช ๐ฆ
โ On) |
81 | | oasuc 8475 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((ฯ ยทo ๐ฅ) โ On โง โช ๐ฆ
โ On) โ ((ฯ ยทo ๐ฅ) +o suc โช ๐ฆ) =
suc ((ฯ ยทo ๐ฅ) +o โช
๐ฆ)) |
82 | 75, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ
((ฯ ยทo ๐ฅ) +o suc โช ๐ฆ) =
suc ((ฯ ยทo ๐ฅ) +o โช
๐ฆ)) |
83 | 71, 82 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ
((ฯ ยทo ๐ฅ) +o ๐ฆ) = suc ((ฯ ยทo ๐ฅ) +o โช ๐ฆ)) |
84 | | limeq 6334 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = suc ((ฯ ยทo ๐ฅ) +o โช ๐ฆ)
โ (Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ) โ Lim suc ((ฯ
ยทo ๐ฅ)
+o โช ๐ฆ))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ (Lim
((ฯ ยทo ๐ฅ) +o ๐ฆ) โ Lim suc ((ฯ
ยทo ๐ฅ)
+o โช ๐ฆ))) |
86 | 50, 85 | mtbird 325 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ On โง ๐ฆ โ ฯ) โง ยฌ
๐ฆ = โ
) โ ยฌ
Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ)) |
87 | 86 | ex 414 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (ยฌ
๐ฆ = โ
โ ยฌ
Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ))) |
88 | 47, 87 | jaod 858 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ ((ยฌ
โ
โ ๐ฅ โจ ยฌ
๐ฆ = โ
) โ ยฌ
Lim ((ฯ ยทo ๐ฅ) +o ๐ฆ))) |
89 | 88 | con2d 134 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (Lim
((ฯ ยทo ๐ฅ) +o ๐ฆ) โ ยฌ (ยฌ โ
โ ๐ฅ โจ ยฌ ๐ฆ = โ
))) |
90 | | anor 982 |
. . . . . . . . . . . . . . . 16
โข ((โ
โ ๐ฅ โง ๐ฆ = โ
) โ ยฌ (ยฌ
โ
โ ๐ฅ โจ ยฌ
๐ฆ =
โ
)) |
91 | 89, 90 | syl6ibr 252 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (Lim
((ฯ ยทo ๐ฅ) +o ๐ฆ) โ (โ
โ ๐ฅ โง ๐ฆ = โ
))) |
92 | 25, 91 | syl9 77 |
. . . . . . . . . . . . . 14
โข
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ด โ ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (Lim ๐ด โ (โ
โ ๐ฅ โง ๐ฆ = โ
)))) |
93 | 92 | com13 88 |
. . . . . . . . . . . . 13
โข (Lim
๐ด โ ((๐ฅ โ On โง ๐ฆ โ ฯ) โ
(((ฯ ยทo ๐ฅ) +o ๐ฆ) = ๐ด โ (โ
โ ๐ฅ โง ๐ฆ = โ
)))) |
94 | 93 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง Lim ๐ด) โ ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด โ (โ
โ ๐ฅ โง ๐ฆ = โ
)))) |
95 | 94 | 3imp 1112 |
. . . . . . . . . . 11
โข (((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ (โ
โ ๐ฅ โง ๐ฆ = โ
)) |
96 | | simp2 1138 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ (๐ฅ โ On โง ๐ฆ โ ฯ)) |
97 | 96, 72 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ ๐ฅ โ On) |
98 | | simpl 484 |
. . . . . . . . . . . . . 14
โข ((โ
โ ๐ฅ โง ๐ฆ = โ
) โ โ
โ ๐ฅ) |
99 | 97, 98 | anim12i 614 |
. . . . . . . . . . . . 13
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ (๐ฅ โ On โง โ
โ ๐ฅ)) |
100 | | ondif1 8452 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (On โ
1o) โ (๐ฅ
โ On โง โ
โ ๐ฅ)) |
101 | 99, 100 | sylibr 233 |
. . . . . . . . . . . 12
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ ๐ฅ โ (On โ
1o)) |
102 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((โ
โ ๐ฅ โง ๐ฆ = โ
) โ ๐ฆ = โ
) |
103 | 102 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข ((โ
โ ๐ฅ โง ๐ฆ = โ
) โ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) =
((ฯ ยทo ๐ฅ) +o โ
)) |
104 | 103 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) =
((ฯ ยทo ๐ฅ) +o โ
)) |
105 | | simpl3 1194 |
. . . . . . . . . . . . 13
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) |
106 | 15, 72, 74 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (ฯ
ยทo ๐ฅ)
โ On) |
107 | | oa0 8467 |
. . . . . . . . . . . . . . 15
โข ((ฯ
ยทo ๐ฅ)
โ On โ ((ฯ ยทo ๐ฅ) +o โ
) = (ฯ
ยทo ๐ฅ)) |
108 | 96, 106, 107 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ ((ฯ
ยทo ๐ฅ)
+o โ
) = (ฯ ยทo ๐ฅ)) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ ((ฯ
ยทo ๐ฅ)
+o โ
) = (ฯ ยทo ๐ฅ)) |
110 | 104, 105,
109 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ ๐ด = (ฯ ยทo ๐ฅ)) |
111 | 101, 110 | jca 513 |
. . . . . . . . . . 11
โข ((((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โง (โ
โ ๐ฅ โง ๐ฆ = โ
)) โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ))) |
112 | 95, 111 | mpdan 686 |
. . . . . . . . . 10
โข (((๐ด โ On โง Lim ๐ด) โง (๐ฅ โ On โง ๐ฆ โ ฯ) โง ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ))) |
113 | 112 | 3exp 1120 |
. . . . . . . . 9
โข ((๐ด โ On โง Lim ๐ด) โ ((๐ฅ โ On โง ๐ฆ โ ฯ) โ (((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ))))) |
114 | 113 | expdimp 454 |
. . . . . . . 8
โข (((๐ด โ On โง Lim ๐ด) โง ๐ฅ โ On) โ (๐ฆ โ ฯ โ (((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ))))) |
115 | 114 | rexlimdv 3151 |
. . . . . . 7
โข (((๐ด โ On โง Lim ๐ด) โง ๐ฅ โ On) โ (โ๐ฆ โ ฯ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ)))) |
116 | 115 | expimpd 455 |
. . . . . 6
โข ((๐ด โ On โง Lim ๐ด) โ ((๐ฅ โ On โง โ๐ฆ โ ฯ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด) โ (๐ฅ โ (On โ 1o) โง
๐ด = (ฯ
ยทo ๐ฅ)))) |
117 | 116 | reximdv2 3162 |
. . . . 5
โข ((๐ด โ On โง Lim ๐ด) โ (โ๐ฅ โ On โ๐ฆ โ ฯ ((ฯ
ยทo ๐ฅ)
+o ๐ฆ) = ๐ด โ โ๐ฅ โ (On โ
1o)๐ด = (ฯ
ยทo ๐ฅ))) |
118 | 23, 117 | mpd 15 |
. . . 4
โข ((๐ด โ On โง Lim ๐ด) โ โ๐ฅ โ (On โ
1o)๐ด = (ฯ
ยทo ๐ฅ)) |
119 | | simpr 486 |
. . . . . . 7
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ ๐ด = (ฯ ยทo ๐ฅ)) |
120 | | eldifi 4091 |
. . . . . . . . 9
โข (๐ฅ โ (On โ
1o) โ ๐ฅ
โ On) |
121 | 15, 120, 74 | sylancr 588 |
. . . . . . . 8
โข (๐ฅ โ (On โ
1o) โ (ฯ ยทo ๐ฅ) โ On) |
122 | 121 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ (ฯ ยทo ๐ฅ) โ On) |
123 | 119, 122 | eqeltrd 2838 |
. . . . . 6
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ ๐ด โ On) |
124 | | limom 7823 |
. . . . . . . . . . 11
โข Lim
ฯ |
125 | 15, 124 | pm3.2i 472 |
. . . . . . . . . 10
โข (ฯ
โ On โง Lim ฯ) |
126 | | omlimcl2 41605 |
. . . . . . . . . 10
โข (((๐ฅ โ On โง (ฯ โ
On โง Lim ฯ)) โง โ
โ ๐ฅ) โ Lim (ฯ ยทo
๐ฅ)) |
127 | 125, 126 | mpanl2 700 |
. . . . . . . . 9
โข ((๐ฅ โ On โง โ
โ
๐ฅ) โ Lim (ฯ
ยทo ๐ฅ)) |
128 | 100, 127 | sylbi 216 |
. . . . . . . 8
โข (๐ฅ โ (On โ
1o) โ Lim (ฯ ยทo ๐ฅ)) |
129 | 128 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ Lim (ฯ ยทo
๐ฅ)) |
130 | | limeq 6334 |
. . . . . . . 8
โข (๐ด = (ฯ ยทo
๐ฅ) โ (Lim ๐ด โ Lim (ฯ
ยทo ๐ฅ))) |
131 | 130 | adantl 483 |
. . . . . . 7
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ (Lim ๐ด โ Lim (ฯ ยทo
๐ฅ))) |
132 | 129, 131 | mpbird 257 |
. . . . . 6
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ Lim ๐ด) |
133 | 123, 132 | jca 513 |
. . . . 5
โข ((๐ฅ โ (On โ
1o) โง ๐ด =
(ฯ ยทo ๐ฅ)) โ (๐ด โ On โง Lim ๐ด)) |
134 | 133 | rexlimiva 3145 |
. . . 4
โข
(โ๐ฅ โ (On
โ 1o)๐ด =
(ฯ ยทo ๐ฅ) โ (๐ด โ On โง Lim ๐ด)) |
135 | 118, 134 | impbii 208 |
. . 3
โข ((๐ด โ On โง Lim ๐ด) โ โ๐ฅ โ (On โ
1o)๐ด = (ฯ
ยทo ๐ฅ)) |
136 | 135 | orbi2i 912 |
. 2
โข ((๐ด = On โจ (๐ด โ On โง Lim ๐ด)) โ (๐ด = On โจ โ๐ฅ โ (On โ 1o)๐ด = (ฯ ยทo
๐ฅ))) |
137 | 8, 13, 136 | 3bitr2i 299 |
1
โข (Lim
๐ด โ (๐ด = On โจ โ๐ฅ โ (On โ 1o)๐ด = (ฯ ยทo
๐ฅ))) |