Step | Hyp | Ref
| Expression |
1 | | n0i 4333 |
. . . . . . 7
โข (๐ด โ (ฯ
โo ๐ถ)
โ ยฌ (ฯ โo ๐ถ) = โ
) |
2 | | fnoe 8507 |
. . . . . . . . 9
โข
โo Fn (On ร On) |
3 | | fndm 6650 |
. . . . . . . . 9
โข (
โo Fn (On ร On) โ dom โo = (On
ร On)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
โข dom
โo = (On ร On) |
5 | 4 | ndmov 7588 |
. . . . . . 7
โข (ยฌ
(ฯ โ On โง ๐ถ
โ On) โ (ฯ โo ๐ถ) = โ
) |
6 | 1, 5 | nsyl2 141 |
. . . . . 6
โข (๐ด โ (ฯ
โo ๐ถ)
โ (ฯ โ On โง ๐ถ โ On)) |
7 | 6 | ad2antrr 725 |
. . . . 5
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (ฯ
โ On โง ๐ถ โ
On)) |
8 | | oecl 8534 |
. . . . 5
โข ((ฯ
โ On โง ๐ถ โ
On) โ (ฯ โo ๐ถ) โ On) |
9 | 7, 8 | syl 17 |
. . . 4
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (ฯ
โo ๐ถ)
โ On) |
10 | | simplr 768 |
. . . 4
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ๐ต โ On) |
11 | | simpr 486 |
. . . 4
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (ฯ
โo ๐ถ)
โ ๐ต) |
12 | | oawordeu 8552 |
. . . 4
โข
((((ฯ โo ๐ถ) โ On โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ
โ!๐ฅ โ On
((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต) |
13 | 9, 10, 11, 12 | syl21anc 837 |
. . 3
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ
โ!๐ฅ โ On
((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต) |
14 | | reurex 3381 |
. . 3
โข
(โ!๐ฅ โ On
((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต โ โ๐ฅ โ On ((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต) |
15 | 13, 14 | syl 17 |
. 2
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ
โ๐ฅ โ On
((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต) |
16 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ๐ด โ (ฯ
โo ๐ถ)) |
17 | | onelon 6387 |
. . . . . . . 8
โข
(((ฯ โo ๐ถ) โ On โง ๐ด โ (ฯ โo ๐ถ)) โ ๐ด โ On) |
18 | 9, 16, 17 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ๐ด โ On) |
19 | 18 | adantr 482 |
. . . . . 6
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ ๐ด โ On) |
20 | 9 | adantr 482 |
. . . . . 6
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ (ฯ
โo ๐ถ)
โ On) |
21 | | simpr 486 |
. . . . . 6
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ ๐ฅ โ On) |
22 | | oaass 8558 |
. . . . . 6
โข ((๐ด โ On โง (ฯ
โo ๐ถ)
โ On โง ๐ฅ โ
On) โ ((๐ด
+o (ฯ โo ๐ถ)) +o ๐ฅ) = (๐ด +o ((ฯ โo
๐ถ) +o ๐ฅ))) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . 5
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ ((๐ด +o (ฯ
โo ๐ถ))
+o ๐ฅ) = (๐ด +o ((ฯ
โo ๐ถ)
+o ๐ฅ))) |
24 | 7 | simprd 497 |
. . . . . . . . . 10
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ๐ถ โ On) |
25 | | eloni 6372 |
. . . . . . . . . 10
โข (๐ถ โ On โ Ord ๐ถ) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ Ord ๐ถ) |
27 | | ordzsl 7831 |
. . . . . . . . 9
โข (Ord
๐ถ โ (๐ถ = โ
โจ โ๐ฅ โ On ๐ถ = suc ๐ฅ โจ Lim ๐ถ)) |
28 | 26, 27 | sylib 217 |
. . . . . . . 8
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (๐ถ = โ
โจ โ๐ฅ โ On ๐ถ = suc ๐ฅ โจ Lim ๐ถ)) |
29 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ ๐ด โ (ฯ
โo ๐ถ)) |
30 | | oveq2 7414 |
. . . . . . . . . . . . . . 15
โข (๐ถ = โ
โ (ฯ
โo ๐ถ) =
(ฯ โo โ
)) |
31 | 7 | simpld 496 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ฯ
โ On) |
32 | | oe0 8519 |
. . . . . . . . . . . . . . . 16
โข (ฯ
โ On โ (ฯ โo โ
) =
1o) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (ฯ
โo โ
) = 1o) |
34 | 30, 33 | sylan9eqr 2795 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ (ฯ
โo ๐ถ) =
1o) |
35 | 29, 34 | eleqtrd 2836 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ ๐ด โ
1o) |
36 | | el1o 8492 |
. . . . . . . . . . . . 13
โข (๐ด โ 1o โ
๐ด =
โ
) |
37 | 35, 36 | sylib 217 |
. . . . . . . . . . . 12
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ ๐ด = โ
) |
38 | 37 | oveq1d 7421 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ (๐ด +o (ฯ
โo ๐ถ)) =
(โ
+o (ฯ โo ๐ถ))) |
39 | 9 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ (ฯ
โo ๐ถ)
โ On) |
40 | | oa0r 8535 |
. . . . . . . . . . . 12
โข ((ฯ
โo ๐ถ)
โ On โ (โ
+o (ฯ โo ๐ถ)) = (ฯ โo
๐ถ)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ (โ
+o (ฯ โo ๐ถ)) = (ฯ โo ๐ถ)) |
42 | 38, 41 | eqtrd 2773 |
. . . . . . . . . 10
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ถ = โ
) โ (๐ด +o (ฯ
โo ๐ถ)) =
(ฯ โo ๐ถ)) |
43 | 42 | ex 414 |
. . . . . . . . 9
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (๐ถ = โ
โ (๐ด +o (ฯ
โo ๐ถ)) =
(ฯ โo ๐ถ))) |
44 | 31 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ ฯ โ On) |
45 | | simprl 770 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ ๐ฅ โ On) |
46 | | oecl 8534 |
. . . . . . . . . . . . . 14
โข ((ฯ
โ On โง ๐ฅ โ
On) โ (ฯ โo ๐ฅ) โ On) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โo ๐ฅ) โ On) |
48 | | limom 7868 |
. . . . . . . . . . . . . 14
โข Lim
ฯ |
49 | 44, 48 | jctir 522 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โ On โง Lim
ฯ)) |
50 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ ๐ด โ (ฯ โo ๐ถ)) |
51 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ ๐ถ = suc ๐ฅ) |
52 | 51 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โo ๐ถ) = (ฯ โo
suc ๐ฅ)) |
53 | | oesuc 8524 |
. . . . . . . . . . . . . . . 16
โข ((ฯ
โ On โง ๐ฅ โ
On) โ (ฯ โo suc ๐ฅ) = ((ฯ โo ๐ฅ) ยทo
ฯ)) |
54 | 44, 45, 53 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โo suc
๐ฅ) = ((ฯ
โo ๐ฅ)
ยทo ฯ)) |
55 | 52, 54 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โo ๐ถ) = ((ฯ โo
๐ฅ) ยทo
ฯ)) |
56 | 50, 55 | eleqtrd 2836 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ ๐ด โ ((ฯ โo ๐ฅ) ยทo
ฯ)) |
57 | | omordlim 8574 |
. . . . . . . . . . . . 13
โข
((((ฯ โo ๐ฅ) โ On โง (ฯ โ On โง
Lim ฯ)) โง ๐ด
โ ((ฯ โo ๐ฅ) ยทo ฯ)) โ
โ๐ฆ โ ฯ
๐ด โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)) |
58 | 47, 49, 56, 57 | syl21anc 837 |
. . . . . . . . . . . 12
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ โ๐ฆ โ ฯ ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) |
59 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (ฯ
โo ๐ฅ)
โ On) |
60 | | nnon 7858 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ ฯ โ ๐ฆ โ On) |
61 | 60 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ๐ฆ โ On) |
62 | | omcl 8533 |
. . . . . . . . . . . . . . . . 17
โข
(((ฯ โo ๐ฅ) โ On โง ๐ฆ โ On) โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
โ On) |
63 | 59, 61, 62 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
โ On) |
64 | | eloni 6372 |
. . . . . . . . . . . . . . . 16
โข
(((ฯ โo ๐ฅ) ยทo ๐ฆ) โ On โ Ord ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ Ord ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)) |
66 | | simprr 772 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) |
67 | | ordelss 6378 |
. . . . . . . . . . . . . . 15
โข ((Ord
((ฯ โo ๐ฅ) ยทo ๐ฆ) โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) โ ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) |
68 | 65, 66, 67 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) |
69 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ๐ด โ On) |
70 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (ฯ
โo ๐ถ)
โ On) |
71 | | oawordri 8547 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ On โง ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
โ On โง (ฯ โo ๐ถ) โ On) โ (๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ (๐ด +o (ฯ โo
๐ถ)) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ถ)))) |
72 | 69, 63, 70, 71 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ (๐ด +o (ฯ โo
๐ถ)) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ถ)))) |
73 | 68, 72 | mpd 15 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (๐ด +o (ฯ โo
๐ถ)) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ถ))) |
74 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ฯ โ
On) |
75 | | odi 8576 |
. . . . . . . . . . . . . . . 16
โข
(((ฯ โo ๐ฅ) โ On โง ๐ฆ โ On โง ฯ โ On) โ
((ฯ โo ๐ฅ) ยทo (๐ฆ +o ฯ)) = (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ((ฯ โo ๐ฅ) ยทo
ฯ))) |
76 | 59, 61, 74, 75 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ((ฯ
โo ๐ฅ)
ยทo (๐ฆ
+o ฯ)) = (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ((ฯ โo
๐ฅ) ยทo
ฯ))) |
77 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ๐ฆ โ ฯ) |
78 | | oaabslem 8643 |
. . . . . . . . . . . . . . . . 17
โข ((ฯ
โ On โง ๐ฆ โ
ฯ) โ (๐ฆ
+o ฯ) = ฯ) |
79 | 74, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (๐ฆ +o ฯ) =
ฯ) |
80 | 79 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ ((ฯ
โo ๐ฅ)
ยทo (๐ฆ
+o ฯ)) = ((ฯ โo ๐ฅ) ยทo
ฯ)) |
81 | 76, 80 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ((ฯ โo ๐ฅ) ยทo ฯ)) = ((ฯ
โo ๐ฅ)
ยทo ฯ)) |
82 | 55 | adantr 482 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (ฯ
โo ๐ถ) =
((ฯ โo ๐ฅ) ยทo
ฯ)) |
83 | 82 | oveq2d 7422 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ถ)) = (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ((ฯ
โo ๐ฅ)
ยทo ฯ))) |
84 | 81, 83, 82 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ถ)) = (ฯ โo ๐ถ)) |
85 | 73, 84 | sseqtrd 4022 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โง (๐ฆ โ ฯ โง ๐ด โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ)) |
86 | 58, 85 | rexlimddv 3162 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ)) |
87 | | oaword2 8550 |
. . . . . . . . . . . . 13
โข
(((ฯ โo ๐ถ) โ On โง ๐ด โ On) โ (ฯ
โo ๐ถ)
โ (๐ด +o
(ฯ โo ๐ถ))) |
88 | 9, 18, 87 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (ฯ
โo ๐ถ)
โ (๐ด +o
(ฯ โo ๐ถ))) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (ฯ โo ๐ถ) โ (๐ด +o (ฯ โo
๐ถ))) |
90 | 86, 89 | eqssd 3999 |
. . . . . . . . . 10
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง (๐ฅ โ On โง ๐ถ = suc ๐ฅ)) โ (๐ด +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
91 | 90 | rexlimdvaa 3157 |
. . . . . . . . 9
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ
(โ๐ฅ โ On ๐ถ = suc ๐ฅ โ (๐ด +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ))) |
92 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ ๐ด โ (ฯ โo ๐ถ)) |
93 | 31 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ ฯ โ
On) |
94 | 24 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ ๐ถ โ On) |
95 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ Lim ๐ถ) |
96 | | oelim2 8592 |
. . . . . . . . . . . . . . 15
โข ((ฯ
โ On โง (๐ถ โ
On โง Lim ๐ถ)) โ
(ฯ โo ๐ถ) = โช
๐ฅ โ (๐ถ โ 1o)(ฯ
โo ๐ฅ)) |
97 | 93, 94, 95, 96 | syl12anc 836 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (ฯ
โo ๐ถ) =
โช ๐ฅ โ (๐ถ โ 1o)(ฯ
โo ๐ฅ)) |
98 | 92, 97 | eleqtrd 2836 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ ๐ด โ โช
๐ฅ โ (๐ถ โ 1o)(ฯ
โo ๐ฅ)) |
99 | | eliun 5001 |
. . . . . . . . . . . . 13
โข (๐ด โ โช ๐ฅ โ (๐ถ โ 1o)(ฯ
โo ๐ฅ)
โ โ๐ฅ โ
(๐ถ โ
1o)๐ด โ
(ฯ โo ๐ฅ)) |
100 | 98, 99 | sylib 217 |
. . . . . . . . . . . 12
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ โ๐ฅ โ (๐ถ โ 1o)๐ด โ (ฯ โo ๐ฅ)) |
101 | | eldifi 4126 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (๐ถ โ 1o) โ ๐ฅ โ ๐ถ) |
102 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ ๐ด โ On) |
103 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (ฯ
โo ๐ถ)
โ On) |
104 | 93 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ ฯ โ
On) |
105 | | 1onn 8636 |
. . . . . . . . . . . . . . . . . . 19
โข
1o โ ฯ |
106 | | ondif2 8499 |
. . . . . . . . . . . . . . . . . . 19
โข (ฯ
โ (On โ 2o) โ (ฯ โ On โง 1o
โ ฯ)) |
107 | 104, 105,
106 | sylanblrc 591 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ ฯ โ (On
โ 2o)) |
108 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ ๐ถ โ On) |
109 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ Lim ๐ถ) |
110 | | oelimcl 8597 |
. . . . . . . . . . . . . . . . . 18
โข ((ฯ
โ (On โ 2o) โง (๐ถ โ On โง Lim ๐ถ)) โ Lim (ฯ โo
๐ถ)) |
111 | 107, 108,
109, 110 | syl12anc 836 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ Lim (ฯ
โo ๐ถ)) |
112 | | oalim 8529 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ On โง ((ฯ
โo ๐ถ)
โ On โง Lim (ฯ โo ๐ถ))) โ (๐ด +o (ฯ โo
๐ถ)) = โช ๐ฆ โ (ฯ โo ๐ถ)(๐ด +o ๐ฆ)) |
113 | 102, 103,
111, 112 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (๐ด +o (ฯ โo
๐ถ)) = โช ๐ฆ โ (ฯ โo ๐ถ)(๐ด +o ๐ฆ)) |
114 | | oelim2 8592 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((ฯ
โ On โง (๐ถ โ
On โง Lim ๐ถ)) โ
(ฯ โo ๐ถ) = โช
๐ง โ (๐ถ โ 1o)(ฯ
โo ๐ง)) |
115 | 93, 94, 95, 114 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (ฯ
โo ๐ถ) =
โช ๐ง โ (๐ถ โ 1o)(ฯ
โo ๐ง)) |
116 | 115 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (๐ฆ โ (ฯ โo ๐ถ) โ ๐ฆ โ โช
๐ง โ (๐ถ โ 1o)(ฯ
โo ๐ง))) |
117 | | eliun 5001 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ โช ๐ง โ (๐ถ โ 1o)(ฯ
โo ๐ง)
โ โ๐ง โ
(๐ถ โ
1o)๐ฆ โ
(ฯ โo ๐ง)) |
118 | 116, 117 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (๐ฆ โ (ฯ โo ๐ถ) โ โ๐ง โ (๐ถ โ 1o)๐ฆ โ (ฯ โo ๐ง))) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (๐ฆ โ (ฯ โo ๐ถ) โ โ๐ง โ (๐ถ โ 1o)๐ฆ โ (ฯ โo ๐ง))) |
120 | | eldifi 4126 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ง โ (๐ถ โ 1o) โ ๐ง โ ๐ถ) |
121 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ฯ โ
On) |
122 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ถ โ On) |
123 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฅ โ ๐ถ) |
124 | | onelon 6387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ถ โ On โง ๐ฅ โ ๐ถ) โ ๐ฅ โ On) |
125 | 122, 123,
124 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฅ โ On) |
126 | 121, 125,
46 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo ๐ฅ)
โ On) |
127 | | eloni 6372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((ฯ
โo ๐ฅ)
โ On โ Ord (ฯ โo ๐ฅ)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ Ord (ฯ
โo ๐ฅ)) |
129 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ด โ (ฯ โo ๐ฅ)) |
130 | | ordelss 6378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((Ord
(ฯ โo ๐ฅ) โง ๐ด โ (ฯ โo ๐ฅ)) โ ๐ด โ (ฯ โo ๐ฅ)) |
131 | 128, 129,
130 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ด โ (ฯ โo ๐ฅ)) |
132 | | ssun1 4172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ๐ฅ โ (๐ฅ โช ๐ง) |
133 | 26 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ Ord ๐ถ) |
134 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ง โ ๐ถ) |
135 | | ordunel 7812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((Ord
๐ถ โง ๐ฅ โ ๐ถ โง ๐ง โ ๐ถ) โ (๐ฅ โช ๐ง) โ ๐ถ) |
136 | 133, 123,
134, 135 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ฅ โช ๐ง) โ ๐ถ) |
137 | | onelon 6387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ถ โ On โง (๐ฅ โช ๐ง) โ ๐ถ) โ (๐ฅ โช ๐ง) โ On) |
138 | 122, 136,
137 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ฅ โช ๐ง) โ On) |
139 | | peano1 7876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข โ
โ ฯ |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ โ
โ
ฯ) |
141 | | oewordi 8588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ฅ โ On โง (๐ฅ โช ๐ง) โ On โง ฯ โ On) โง
โ
โ ฯ) โ (๐ฅ โ (๐ฅ โช ๐ง) โ (ฯ โo ๐ฅ) โ (ฯ
โo (๐ฅ โช
๐ง)))) |
142 | 125, 138,
121, 140, 141 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ฅ โ (๐ฅ โช ๐ง) โ (ฯ โo ๐ฅ) โ (ฯ
โo (๐ฅ โช
๐ง)))) |
143 | 132, 142 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo ๐ฅ)
โ (ฯ โo (๐ฅ โช ๐ง))) |
144 | 131, 143 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ด โ (ฯ โo (๐ฅ โช ๐ง))) |
145 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ด โ On) |
146 | | oecl 8534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((ฯ
โ On โง (๐ฅ โช
๐ง) โ On) โ
(ฯ โo (๐ฅ โช ๐ง)) โ On) |
147 | 121, 138,
146 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo (๐ฅ โช
๐ง)) โ
On) |
148 | | onelon 6387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ถ โ On โง ๐ง โ ๐ถ) โ ๐ง โ On) |
149 | 122, 134,
148 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ง โ On) |
150 | | oecl 8534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((ฯ
โ On โง ๐ง โ
On) โ (ฯ โo ๐ง) โ On) |
151 | 121, 149,
150 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo ๐ง)
โ On) |
152 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฆ โ (ฯ โo ๐ง)) |
153 | | onelon 6387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((ฯ โo ๐ง) โ On โง ๐ฆ โ (ฯ โo ๐ง)) โ ๐ฆ โ On) |
154 | 151, 152,
153 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฆ โ On) |
155 | | oawordri 8547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ด โ On โง (ฯ
โo (๐ฅ โช
๐ง)) โ On โง ๐ฆ โ On) โ (๐ด โ (ฯ
โo (๐ฅ โช
๐ง)) โ (๐ด +o ๐ฆ) โ ((ฯ
โo (๐ฅ โช
๐ง)) +o ๐ฆ))) |
156 | 145, 147,
154, 155 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ด โ (ฯ โo (๐ฅ โช ๐ง)) โ (๐ด +o ๐ฆ) โ ((ฯ โo (๐ฅ โช ๐ง)) +o ๐ฆ))) |
157 | 144, 156 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ด +o ๐ฆ) โ ((ฯ โo (๐ฅ โช ๐ง)) +o ๐ฆ)) |
158 | | eloni 6372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((ฯ
โo ๐ง)
โ On โ Ord (ฯ โo ๐ง)) |
159 | 151, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ Ord (ฯ
โo ๐ง)) |
160 | | ordelss 6378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((Ord
(ฯ โo ๐ง) โง ๐ฆ โ (ฯ โo ๐ง)) โ ๐ฆ โ (ฯ โo ๐ง)) |
161 | 159, 152,
160 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฆ โ (ฯ โo ๐ง)) |
162 | | ssun2 4173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ๐ง โ (๐ฅ โช ๐ง) |
163 | | oewordi 8588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ง โ On โง (๐ฅ โช ๐ง) โ On โง ฯ โ On) โง
โ
โ ฯ) โ (๐ง โ (๐ฅ โช ๐ง) โ (ฯ โo ๐ง) โ (ฯ
โo (๐ฅ โช
๐ง)))) |
164 | 149, 138,
121, 140, 163 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ง โ (๐ฅ โช ๐ง) โ (ฯ โo ๐ง) โ (ฯ
โo (๐ฅ โช
๐ง)))) |
165 | 162, 164 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo ๐ง)
โ (ฯ โo (๐ฅ โช ๐ง))) |
166 | 161, 165 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ๐ฆ โ (ฯ โo (๐ฅ โช ๐ง))) |
167 | | oaword 8546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ On โง (ฯ
โo (๐ฅ โช
๐ง)) โ On โง
(ฯ โo (๐ฅ โช ๐ง)) โ On) โ (๐ฆ โ (ฯ โo (๐ฅ โช ๐ง)) โ ((ฯ โo (๐ฅ โช ๐ง)) +o ๐ฆ) โ ((ฯ โo (๐ฅ โช ๐ง)) +o (ฯ โo
(๐ฅ โช ๐ง))))) |
168 | 154, 147,
147, 167 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ฆ โ (ฯ โo (๐ฅ โช ๐ง)) โ ((ฯ โo (๐ฅ โช ๐ง)) +o ๐ฆ) โ ((ฯ โo (๐ฅ โช ๐ง)) +o (ฯ โo
(๐ฅ โช ๐ง))))) |
169 | 166, 168 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) +o ๐ฆ) โ ((ฯ
โo (๐ฅ โช
๐ง)) +o (ฯ
โo (๐ฅ โช
๐ง)))) |
170 | 157, 169 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ด +o ๐ฆ) โ ((ฯ โo (๐ฅ โช ๐ง)) +o (ฯ โo
(๐ฅ โช ๐ง)))) |
171 | | ordom 7862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข Ord
ฯ |
172 | | ordsucss 7803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (Ord
ฯ โ (1o โ ฯ โ suc 1o โ
ฯ)) |
173 | 171, 105,
172 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข suc
1o โ ฯ |
174 | | 1on 8475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
1o โ On |
175 | | onsuc 7796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(1o โ On โ suc 1o โ
On) |
176 | 174, 175 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ suc 1o
โ On) |
177 | | omwordi 8568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((suc
1o โ On โง ฯ โ On โง (ฯ
โo (๐ฅ โช
๐ง)) โ On) โ (suc
1o โ ฯ โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo suc 1o)
โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo
ฯ))) |
178 | 176, 121,
147, 177 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (suc 1o
โ ฯ โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo suc 1o)
โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo
ฯ))) |
179 | 173, 178 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) ยทo
suc 1o) โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo
ฯ)) |
180 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ 1o โ
On) |
181 | | omsuc 8523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((ฯ โo (๐ฅ โช ๐ง)) โ On โง 1o โ On)
โ ((ฯ โo (๐ฅ โช ๐ง)) ยทo suc 1o) =
(((ฯ โo (๐ฅ โช ๐ง)) ยทo 1o)
+o (ฯ โo (๐ฅ โช ๐ง)))) |
182 | 147, 180,
181 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) ยทo
suc 1o) = (((ฯ โo (๐ฅ โช ๐ง)) ยทo 1o)
+o (ฯ โo (๐ฅ โช ๐ง)))) |
183 | | om1 8539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((ฯ
โo (๐ฅ โช
๐ง)) โ On โ
((ฯ โo (๐ฅ โช ๐ง)) ยทo 1o) =
(ฯ โo (๐ฅ โช ๐ง))) |
184 | 147, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) ยทo
1o) = (ฯ โo (๐ฅ โช ๐ง))) |
185 | 184 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (((ฯ
โo (๐ฅ โช
๐ง)) ยทo
1o) +o (ฯ โo (๐ฅ โช ๐ง))) = ((ฯ โo (๐ฅ โช ๐ง)) +o (ฯ โo
(๐ฅ โช ๐ง)))) |
186 | 182, 185 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) +o (ฯ
โo (๐ฅ โช
๐ง))) = ((ฯ
โo (๐ฅ โช
๐ง)) ยทo
suc 1o)) |
187 | | oesuc 8524 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((ฯ
โ On โง (๐ฅ โช
๐ง) โ On) โ
(ฯ โo suc (๐ฅ โช ๐ง)) = ((ฯ โo (๐ฅ โช ๐ง)) ยทo
ฯ)) |
188 | 121, 138,
187 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo suc (๐ฅ
โช ๐ง)) = ((ฯ
โo (๐ฅ โช
๐ง)) ยทo
ฯ)) |
189 | 179, 186,
188 | 3sstr4d 4029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ ((ฯ
โo (๐ฅ โช
๐ง)) +o (ฯ
โo (๐ฅ โช
๐ง))) โ (ฯ
โo suc (๐ฅ
โช ๐ง))) |
190 | 170, 189 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ด +o ๐ฆ) โ (ฯ โo suc
(๐ฅ โช ๐ง))) |
191 | | ordsucss 7803 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (Ord
๐ถ โ ((๐ฅ โช ๐ง) โ ๐ถ โ suc (๐ฅ โช ๐ง) โ ๐ถ)) |
192 | 133, 136,
191 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ suc (๐ฅ โช ๐ง) โ ๐ถ) |
193 | | onsuc 7796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฅ โช ๐ง) โ On โ suc (๐ฅ โช ๐ง) โ On) |
194 | 138, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ suc (๐ฅ โช ๐ง) โ On) |
195 | | oewordi 8588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((suc
(๐ฅ โช ๐ง) โ On โง ๐ถ โ On โง ฯ โ On) โง
โ
โ ฯ) โ (suc (๐ฅ โช ๐ง) โ ๐ถ โ (ฯ โo suc
(๐ฅ โช ๐ง)) โ (ฯ โo ๐ถ))) |
196 | 194, 122,
121, 140, 195 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (suc (๐ฅ โช ๐ง) โ ๐ถ โ (ฯ โo suc
(๐ฅ โช ๐ง)) โ (ฯ โo ๐ถ))) |
197 | 192, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (ฯ
โo suc (๐ฅ
โช ๐ง)) โ (ฯ
โo ๐ถ)) |
198 | 190, 197 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง (๐ง โ ๐ถ โง ๐ฆ โ (ฯ โo ๐ง))) โ (๐ด +o ๐ฆ) โ (ฯ โo ๐ถ)) |
199 | 198 | expr 458 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง ๐ง โ ๐ถ) โ (๐ฆ โ (ฯ โo ๐ง) โ (๐ด +o ๐ฆ) โ (ฯ โo ๐ถ))) |
200 | 120, 199 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โง ๐ง โ (๐ถ โ 1o)) โ (๐ฆ โ (ฯ
โo ๐ง)
โ (๐ด +o
๐ฆ) โ (ฯ
โo ๐ถ))) |
201 | 200 | rexlimdva 3156 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (โ๐ง โ (๐ถ โ 1o)๐ฆ โ (ฯ โo ๐ง) โ (๐ด +o ๐ฆ) โ (ฯ โo ๐ถ))) |
202 | 119, 201 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (๐ฆ โ (ฯ โo ๐ถ) โ (๐ด +o ๐ฆ) โ (ฯ โo ๐ถ))) |
203 | 202 | ralrimiv 3146 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ โ๐ฆ โ (ฯ
โo ๐ถ)(๐ด +o ๐ฆ) โ (ฯ
โo ๐ถ)) |
204 | | iunss 5048 |
. . . . . . . . . . . . . . . . 17
โข (โช ๐ฆ โ (ฯ โo ๐ถ)(๐ด +o ๐ฆ) โ (ฯ โo ๐ถ) โ โ๐ฆ โ (ฯ
โo ๐ถ)(๐ด +o ๐ฆ) โ (ฯ
โo ๐ถ)) |
205 | 203, 204 | sylibr 233 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ โช ๐ฆ โ (ฯ โo ๐ถ)(๐ด +o ๐ฆ) โ (ฯ โo ๐ถ)) |
206 | 113, 205 | eqsstrd 4020 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง (๐ฅ โ ๐ถ โง ๐ด โ (ฯ โo ๐ฅ))) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ)) |
207 | 206 | expr 458 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง ๐ฅ โ ๐ถ) โ (๐ด โ (ฯ โo ๐ฅ) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ))) |
208 | 101, 207 | sylan2 594 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
(ฯ โo ๐ถ) โง ๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โง ๐ฅ โ (๐ถ โ 1o)) โ (๐ด โ (ฯ
โo ๐ฅ)
โ (๐ด +o
(ฯ โo ๐ถ)) โ (ฯ โo ๐ถ))) |
209 | 208 | rexlimdva 3156 |
. . . . . . . . . . . 12
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (โ๐ฅ โ (๐ถ โ 1o)๐ด โ (ฯ โo ๐ฅ) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ))) |
210 | 100, 209 | mpd 15 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (๐ด +o (ฯ โo
๐ถ)) โ (ฯ
โo ๐ถ)) |
211 | 88 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (ฯ
โo ๐ถ)
โ (๐ด +o
(ฯ โo ๐ถ))) |
212 | 210, 211 | eqssd 3999 |
. . . . . . . . . 10
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง Lim ๐ถ) โ (๐ด +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
213 | 212 | ex 414 |
. . . . . . . . 9
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (Lim
๐ถ โ (๐ด +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ))) |
214 | 43, 91, 213 | 3jaod 1429 |
. . . . . . . 8
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ ((๐ถ = โ
โจ โ๐ฅ โ On ๐ถ = suc ๐ฅ โจ Lim ๐ถ) โ (๐ด +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ))) |
215 | 28, 214 | mpd 15 |
. . . . . . 7
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (๐ด +o (ฯ
โo ๐ถ)) =
(ฯ โo ๐ถ)) |
216 | 215 | adantr 482 |
. . . . . 6
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ (๐ด +o (ฯ
โo ๐ถ)) =
(ฯ โo ๐ถ)) |
217 | 216 | oveq1d 7421 |
. . . . 5
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ ((๐ด +o (ฯ
โo ๐ถ))
+o ๐ฅ) =
((ฯ โo ๐ถ) +o ๐ฅ)) |
218 | 23, 217 | eqtr3d 2775 |
. . . 4
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ (๐ด +o ((ฯ
โo ๐ถ)
+o ๐ฅ)) =
((ฯ โo ๐ถ) +o ๐ฅ)) |
219 | | oveq2 7414 |
. . . . 5
โข
(((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต โ (๐ด +o ((ฯ โo
๐ถ) +o ๐ฅ)) = (๐ด +o ๐ต)) |
220 | | id 22 |
. . . . 5
โข
(((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต โ ((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต) |
221 | 219, 220 | eqeq12d 2749 |
. . . 4
โข
(((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต โ ((๐ด +o ((ฯ โo
๐ถ) +o ๐ฅ)) = ((ฯ
โo ๐ถ)
+o ๐ฅ) โ
(๐ด +o ๐ต) = ๐ต)) |
222 | 218, 221 | syl5ibcom 244 |
. . 3
โข ((((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โง ๐ฅ โ On) โ (((ฯ
โo ๐ถ)
+o ๐ฅ) = ๐ต โ (๐ด +o ๐ต) = ๐ต)) |
223 | 222 | rexlimdva 3156 |
. 2
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ
(โ๐ฅ โ On
((ฯ โo ๐ถ) +o ๐ฅ) = ๐ต โ (๐ด +o ๐ต) = ๐ต)) |
224 | 15, 223 | mpd 15 |
1
โข (((๐ด โ (ฯ
โo ๐ถ) โง
๐ต โ On) โง (ฯ
โo ๐ถ)
โ ๐ต) โ (๐ด +o ๐ต) = ๐ต) |