Step | Hyp | Ref
| Expression |
1 | | eleq2 2823 |
. . . . . . . 8
โข (๐ฅ = โ
โ (โ
โ ๐ฅ โ โ
โ โ
)) |
2 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ฅ = โ
โ (ฯ
โo ๐ฅ) =
(ฯ โo โ
)) |
3 | 2 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ฅ = โ
โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(๐ด ยทo
(ฯ โo โ
))) |
4 | 3, 2 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = โ
โ ((๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ) โ (๐ด ยทo (ฯ
โo โ
)) = (ฯ โo
โ
))) |
5 | 1, 4 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = โ
โ ((โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) โ (โ
โ โ
โ
(๐ด ยทo
(ฯ โo โ
)) = (ฯ โo
โ
)))) |
6 | | eleq2 2823 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (โ
โ ๐ฅ โ โ
โ ๐ฆ)) |
7 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (ฯ โo ๐ฅ) = (ฯ โo
๐ฆ)) |
8 | 7 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(๐ด ยทo
(ฯ โo ๐ฆ))) |
9 | 8, 7 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ) โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) |
10 | 6, 9 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ ((โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) โ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)))) |
11 | | eleq2 2823 |
. . . . . . . 8
โข (๐ฅ = suc ๐ฆ โ (โ
โ ๐ฅ โ โ
โ suc ๐ฆ)) |
12 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ฅ = suc ๐ฆ โ (ฯ โo ๐ฅ) = (ฯ โo
suc ๐ฆ)) |
13 | 12 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(๐ด ยทo
(ฯ โo suc ๐ฆ))) |
14 | 13, 12 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ) โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ))) |
15 | 11, 14 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = suc ๐ฆ โ ((โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) โ (โ
โ suc ๐ฆ โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
16 | | eleq2 2823 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ (โ
โ ๐ฅ โ โ
โ ๐ต)) |
17 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ฅ = ๐ต โ (ฯ โo ๐ฅ) = (ฯ โo
๐ต)) |
18 | 17 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ฅ = ๐ต โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(๐ด ยทo
(ฯ โo ๐ต))) |
19 | 18, 17 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ ((๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ) โ (๐ด ยทo (ฯ
โo ๐ต)) =
(ฯ โo ๐ต))) |
20 | 16, 19 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = ๐ต โ ((โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) โ (โ
โ ๐ต โ (๐ด ยทo (ฯ
โo ๐ต)) =
(ฯ โo ๐ต)))) |
21 | | noel 4331 |
. . . . . . . . 9
โข ยฌ
โ
โ โ
|
22 | 21 | pm2.21i 119 |
. . . . . . . 8
โข (โ
โ โ
โ (๐ด
ยทo (ฯ โo โ
)) = (ฯ
โo โ
)) |
23 | 22 | a1i 11 |
. . . . . . 7
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โ (โ
โ โ
โ (๐ด ยทo (ฯ
โo โ
)) = (ฯ โo
โ
))) |
24 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ฯ โ On) |
25 | | simpll 766 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ๐ด โ
ฯ) |
26 | | simplr 768 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ โ
โ ๐ด) |
27 | | omabslem 8649 |
. . . . . . . . . . . . . . . 16
โข ((ฯ
โ On โง ๐ด โ
ฯ โง โ
โ ๐ด) โ (๐ด ยทo ฯ) =
ฯ) |
28 | 24, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ด
ยทo ฯ) = ฯ) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โง ๐ฆ = โ
)
โ (๐ด
ยทo ฯ) = ฯ) |
30 | | suceq 6431 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = โ
โ suc ๐ฆ = suc โ
) |
31 | | df-1o 8466 |
. . . . . . . . . . . . . . . . . 18
โข
1o = suc โ
|
32 | 30, 31 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = โ
โ suc ๐ฆ =
1o) |
33 | 32 | oveq2d 7425 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = โ
โ (ฯ
โo suc ๐ฆ) =
(ฯ โo 1o)) |
34 | | oe1 8544 |
. . . . . . . . . . . . . . . . 17
โข (ฯ
โ On โ (ฯ โo 1o) =
ฯ) |
35 | 34 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (ฯ โo 1o) =
ฯ) |
36 | 33, 35 | sylan9eqr 2795 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โง ๐ฆ = โ
)
โ (ฯ โo suc ๐ฆ) = ฯ) |
37 | 36 | oveq2d 7425 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โง ๐ฆ = โ
)
โ (๐ด
ยทo (ฯ โo suc ๐ฆ)) = (๐ด ยทo
ฯ)) |
38 | 29, 37, 36 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โง ๐ฆ = โ
)
โ (๐ด
ยทo (ฯ โo suc ๐ฆ)) = (ฯ โo suc ๐ฆ)) |
39 | 38 | ex 414 |
. . . . . . . . . . . 12
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ฆ = โ
โ (๐ด
ยทo (ฯ โo suc ๐ฆ)) = (ฯ โo suc ๐ฆ))) |
40 | 39 | a1dd 50 |
. . . . . . . . . . 11
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ฆ = โ
โ ((โ
โ ๐ฆ
โ (๐ด
ยทo (ฯ โo ๐ฆ)) = (ฯ โo ๐ฆ)) โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
41 | | oveq1 7416 |
. . . . . . . . . . . . . 14
โข ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โ ((๐ด ยทo (ฯ
โo ๐ฆ))
ยทo ฯ) = ((ฯ โo ๐ฆ) ยทo
ฯ)) |
42 | | oesuc 8527 |
. . . . . . . . . . . . . . . . . 18
โข ((ฯ
โ On โง ๐ฆ โ
On) โ (ฯ โo suc ๐ฆ) = ((ฯ โo ๐ฆ) ยทo
ฯ)) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (ฯ โo suc ๐ฆ) = ((ฯ โo ๐ฆ) ยทo
ฯ)) |
44 | 43 | oveq2d 7425 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ด
ยทo (ฯ โo suc ๐ฆ)) = (๐ด ยทo ((ฯ
โo ๐ฆ)
ยทo ฯ))) |
45 | | nnon 7861 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ ฯ โ ๐ด โ On) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ๐ด โ
On) |
47 | | oecl 8537 |
. . . . . . . . . . . . . . . . . 18
โข ((ฯ
โ On โง ๐ฆ โ
On) โ (ฯ โo ๐ฆ) โ On) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (ฯ โo ๐ฆ) โ On) |
49 | | omass 8580 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ On โง (ฯ
โo ๐ฆ)
โ On โง ฯ โ On) โ ((๐ด ยทo (ฯ
โo ๐ฆ))
ยทo ฯ) = (๐ด ยทo ((ฯ
โo ๐ฆ)
ยทo ฯ))) |
50 | 46, 48, 24, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((๐ด
ยทo (ฯ โo ๐ฆ)) ยทo ฯ) = (๐ด ยทo ((ฯ
โo ๐ฆ)
ยทo ฯ))) |
51 | 44, 50 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ด
ยทo (ฯ โo suc ๐ฆ)) = ((๐ด ยทo (ฯ
โo ๐ฆ))
ยทo ฯ)) |
52 | 51, 43 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((๐ด
ยทo (ฯ โo suc ๐ฆ)) = (ฯ โo suc ๐ฆ) โ ((๐ด ยทo (ฯ
โo ๐ฆ))
ยทo ฯ) = ((ฯ โo ๐ฆ) ยทo
ฯ))) |
53 | 41, 52 | imbitrrid 245 |
. . . . . . . . . . . . 13
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((๐ด
ยทo (ฯ โo ๐ฆ)) = (ฯ โo ๐ฆ) โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ))) |
54 | 53 | imim2d 57 |
. . . . . . . . . . . 12
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
55 | 54 | com23 86 |
. . . . . . . . . . 11
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (โ
โ ๐ฆ โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
56 | | simprr 772 |
. . . . . . . . . . . 12
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ๐ฆ โ
On) |
57 | | on0eqel 6489 |
. . . . . . . . . . . 12
โข (๐ฆ โ On โ (๐ฆ = โ
โจ โ
โ
๐ฆ)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ (๐ฆ = โ
โจ โ
โ ๐ฆ)) |
59 | 40, 55, 58 | mpjaod 859 |
. . . . . . . . . 10
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ))) |
60 | 59 | a1dd 50 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ฆ โ
On)) โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ suc ๐ฆ โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
61 | 60 | anassrs 469 |
. . . . . . . 8
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โง ๐ฆ โ
On) โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ suc ๐ฆ โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ)))) |
62 | 61 | expcom 415 |
. . . . . . 7
โข (๐ฆ โ On โ (((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ suc ๐ฆ โ (๐ด ยทo (ฯ
โo suc ๐ฆ))
= (ฯ โo suc ๐ฆ))))) |
63 | 45 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ ๐ด โ On) |
64 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ ฯ โ On) |
65 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ Lim ๐ฅ) |
66 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
โข ๐ฅ โ V |
67 | 65, 66 | jctil 521 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ (๐ฅ โ V โง
Lim ๐ฅ)) |
68 | | limelon 6429 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ V โง Lim ๐ฅ) โ ๐ฅ โ On) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ ๐ฅ โ
On) |
70 | | oecl 8537 |
. . . . . . . . . . . . . . . 16
โข ((ฯ
โ On โง ๐ฅ โ
On) โ (ฯ โo ๐ฅ) โ On) |
71 | 64, 69, 70 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ (ฯ โo ๐ฅ) โ On) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (ฯ โo ๐ฅ) โ On) |
73 | | 1onn 8639 |
. . . . . . . . . . . . . . . . 17
โข
1o โ ฯ |
74 | | ondif2 8502 |
. . . . . . . . . . . . . . . . 17
โข (ฯ
โ (On โ 2o) โ (ฯ โ On โง 1o
โ ฯ)) |
75 | 64, 73, 74 | sylanblrc 591 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ ฯ โ (On โ 2o)) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ ฯ โ (On โ
2o)) |
77 | 67 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ฅ โ V โง Lim ๐ฅ)) |
78 | | oelimcl 8600 |
. . . . . . . . . . . . . . 15
โข ((ฯ
โ (On โ 2o) โง (๐ฅ โ V โง Lim ๐ฅ)) โ Lim (ฯ โo
๐ฅ)) |
79 | 76, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ Lim (ฯ โo
๐ฅ)) |
80 | | omlim 8533 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ((ฯ
โo ๐ฅ)
โ On โง Lim (ฯ โo ๐ฅ))) โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
โช ๐ง โ (ฯ โo ๐ฅ)(๐ด ยทo ๐ง)) |
81 | 63, 72, 79, 80 | syl12anc 836 |
. . . . . . . . . . . . 13
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
โช ๐ง โ (ฯ โo ๐ฅ)(๐ด ยทo ๐ง)) |
82 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ ฯ โ
On) |
83 | | oelim2 8595 |
. . . . . . . . . . . . . . . . . . . 20
โข ((ฯ
โ On โง (๐ฅ โ V
โง Lim ๐ฅ)) โ
(ฯ โo ๐ฅ) = โช ๐ฆ โ (๐ฅ โ 1o)(ฯ
โo ๐ฆ)) |
84 | 82, 77, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (ฯ โo ๐ฅ) = โช ๐ฆ โ (๐ฅ โ 1o)(ฯ
โo ๐ฆ)) |
85 | 84 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ง โ (ฯ โo ๐ฅ) โ ๐ง โ โช
๐ฆ โ (๐ฅ โ 1o)(ฯ
โo ๐ฆ))) |
86 | | eliun 5002 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง โ โช ๐ฆ โ (๐ฅ โ 1o)(ฯ
โo ๐ฆ)
โ โ๐ฆ โ
(๐ฅ โ
1o)๐ง โ
(ฯ โo ๐ฆ)) |
87 | 85, 86 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ง โ (ฯ โo ๐ฅ) โ โ๐ฆ โ (๐ฅ โ 1o)๐ง โ (ฯ โo ๐ฆ))) |
88 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ ๐ฅ โ On) |
89 | | anass 470 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ โ ๐ฅ โง โ
โ ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ)) โ (๐ฆ โ ๐ฅ โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)))) |
90 | | onelon 6390 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ โ On โง ๐ฆ โ ๐ฅ) โ ๐ฆ โ On) |
91 | | on0eln0 6421 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ โ On โ (โ
โ ๐ฆ โ ๐ฆ โ โ
)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ On โง ๐ฆ โ ๐ฅ) โ (โ
โ ๐ฆ โ ๐ฆ โ โ
)) |
93 | 92 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ On โ ((๐ฆ โ ๐ฅ โง โ
โ ๐ฆ) โ (๐ฆ โ ๐ฅ โง ๐ฆ โ โ
))) |
94 | | dif1o 8500 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ (๐ฅ โ 1o) โ (๐ฆ โ ๐ฅ โง ๐ฆ โ โ
)) |
95 | 93, 94 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ On โ ((๐ฆ โ ๐ฅ โง โ
โ ๐ฆ) โ ๐ฆ โ (๐ฅ โ 1o))) |
96 | 95 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ On โ (((๐ฆ โ ๐ฅ โง โ
โ ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ)) โ (๐ฆ โ (๐ฅ โ 1o) โง ๐ง โ (ฯ
โo ๐ฆ)))) |
97 | 89, 96 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ On โ ((๐ฆ โ ๐ฅ โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ฆ โ (๐ฅ โ 1o) โง ๐ง โ (ฯ
โo ๐ฆ)))) |
98 | 97 | rexbidv2 3175 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ On โ (โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)) โ โ๐ฆ โ (๐ฅ โ 1o)๐ง โ (ฯ โo ๐ฆ))) |
99 | 88, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)) โ โ๐ฆ โ (๐ฅ โ 1o)๐ง โ (ฯ โo ๐ฆ))) |
100 | 87, 99 | bitr4d 282 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ง โ (ฯ โo ๐ฅ) โ โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)))) |
101 | | r19.29 3115 |
. . . . . . . . . . . . . . . . . 18
โข
((โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โง โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ โ๐ฆ โ ๐ฅ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)))) |
102 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) |
103 | 102 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((โ
โ ๐ฆ
โ (๐ด
ยทo (ฯ โo ๐ฆ)) = (ฯ โo ๐ฆ)) โง โ
โ ๐ฆ) โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) |
104 | 103 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((โ
โ ๐ฆ
โ (๐ด
ยทo (ฯ โo ๐ฆ)) = (ฯ โo ๐ฆ)) โง โ
โ ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ)) โ ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) |
105 | 104 | anasss 468 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((โ
โ ๐ฆ
โ (๐ด
ยทo (ฯ โo ๐ฆ)) = (ฯ โo ๐ฆ)) โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) |
106 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (ฯ
โo ๐ฅ)
โ On) |
107 | | eloni 6375 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((ฯ
โo ๐ฅ)
โ On โ Ord (ฯ โo ๐ฅ)) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ Ord (ฯ
โo ๐ฅ)) |
109 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ง โ (ฯ โo ๐ฆ)) |
110 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ฯ โ
On) |
111 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ฅ โ On) |
112 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ฆ โ ๐ฅ) |
113 | 111, 112,
90 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ฆ โ On) |
114 | 110, 113,
47 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (ฯ
โo ๐ฆ)
โ On) |
115 | | onelon 6390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((ฯ โo ๐ฆ) โ On โง ๐ง โ (ฯ โo ๐ฆ)) โ ๐ง โ On) |
116 | 114, 109,
115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ง โ On) |
117 | 45 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ ๐ด โ
On) |
118 | 117 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ๐ด โ On) |
119 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ โ
โ ๐ด) |
120 | 119 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ โ
โ ๐ด) |
121 | | omord2 8567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ง โ On โง (ฯ
โo ๐ฆ)
โ On โง ๐ด โ
On) โง โ
โ ๐ด)
โ (๐ง โ (ฯ
โo ๐ฆ)
โ (๐ด
ยทo ๐ง)
โ (๐ด
ยทo (ฯ โo ๐ฆ)))) |
122 | 116, 114,
118, 120, 121 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ง โ (ฯ โo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (ฯ
โo ๐ฆ)))) |
123 | 109, 122 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (ฯ
โo ๐ฆ))) |
124 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) |
125 | 123, 124 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฆ)) |
126 | 75 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ ฯ โ (On
โ 2o)) |
127 | | oeord 8588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ On โง ๐ฅ โ On โง ฯ โ
(On โ 2o)) โ (๐ฆ โ ๐ฅ โ (ฯ โo ๐ฆ) โ (ฯ
โo ๐ฅ))) |
128 | 113, 111,
126, 127 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ฆ โ ๐ฅ โ (ฯ โo ๐ฆ) โ (ฯ
โo ๐ฅ))) |
129 | 112, 128 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (ฯ
โo ๐ฆ)
โ (ฯ โo ๐ฅ)) |
130 | | ontr1 6411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((ฯ
โo ๐ฅ)
โ On โ (((๐ด
ยทo ๐ง)
โ (ฯ โo ๐ฆ) โง (ฯ โo ๐ฆ) โ (ฯ
โo ๐ฅ))
โ (๐ด
ยทo ๐ง)
โ (ฯ โo ๐ฅ))) |
131 | 106, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (((๐ด ยทo ๐ง) โ (ฯ โo ๐ฆ) โง (ฯ
โo ๐ฆ)
โ (ฯ โo ๐ฅ)) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
132 | 125, 129,
131 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) |
133 | | ordelss 6381 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((Ord
(ฯ โo ๐ฅ) โง (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) |
134 | 108, 132,
133 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ
ฯ โง โ
โ ๐ด) โง (ฯ โ On โง Lim ๐ฅ)) โง ๐ฆ โ ๐ฅ) โง ((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) |
135 | 134 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง ๐ฆ โ ๐ฅ) โ (((๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ) โง ๐ง โ (ฯ โo ๐ฆ)) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
136 | 105, 135 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง ๐ฆ โ ๐ฅ) โ (((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
137 | 136 | rexlimdva 3156 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ (โ๐ฆ โ
๐ฅ ((โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โง (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
138 | 101, 137 | syl5 34 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ ((โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โง โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ))) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
139 | 138 | expdimp 454 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โง ๐ง โ (ฯ โo ๐ฆ)) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
140 | 100, 139 | sylbid 239 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ง โ (ฯ โo ๐ฅ) โ (๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ))) |
141 | 140 | ralrimiv 3146 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ โ๐ง โ (ฯ โo ๐ฅ)(๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) |
142 | | iunss 5049 |
. . . . . . . . . . . . . 14
โข (โช ๐ง โ (ฯ โo ๐ฅ)(๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ) โ โ๐ง โ (ฯ
โo ๐ฅ)(๐ด ยทo ๐ง) โ (ฯ
โo ๐ฅ)) |
143 | 141, 142 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ โช ๐ง โ (ฯ โo ๐ฅ)(๐ด ยทo ๐ง) โ (ฯ โo ๐ฅ)) |
144 | 81, 143 | eqsstrd 4021 |
. . . . . . . . . . . 12
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ด ยทo (ฯ
โo ๐ฅ))
โ (ฯ โo ๐ฅ)) |
145 | | simpllr 775 |
. . . . . . . . . . . . 13
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ โ
โ ๐ด) |
146 | | omword2 8574 |
. . . . . . . . . . . . 13
โข
((((ฯ โo ๐ฅ) โ On โง ๐ด โ On) โง โ
โ ๐ด) โ (ฯ
โo ๐ฅ)
โ (๐ด
ยทo (ฯ โo ๐ฅ))) |
147 | 72, 63, 145, 146 | syl21anc 837 |
. . . . . . . . . . . 12
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (ฯ โo ๐ฅ) โ (๐ด ยทo (ฯ
โo ๐ฅ))) |
148 | 144, 147 | eqssd 4000 |
. . . . . . . . . . 11
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โง โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ))) โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) |
149 | 148 | ex 414 |
. . . . . . . . . 10
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง Lim ๐ฅ))
โ (โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ))) |
150 | 149 | anassrs 469 |
. . . . . . . . 9
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โง Lim ๐ฅ)
โ (โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ))) |
151 | 150 | a1dd 50 |
. . . . . . . 8
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โง Lim ๐ฅ)
โ (โ๐ฆ โ
๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)))) |
152 | 151 | expcom 415 |
. . . . . . 7
โข (Lim
๐ฅ โ (((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โ (โ๐ฆ โ ๐ฅ (โ
โ ๐ฆ โ (๐ด ยทo (ฯ
โo ๐ฆ)) =
(ฯ โo ๐ฆ)) โ (โ
โ ๐ฅ โ (๐ด ยทo (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ))))) |
153 | 5, 10, 15, 20, 23, 62, 152 | tfinds3 7854 |
. . . . . 6
โข (๐ต โ On โ (((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โ (โ
โ ๐ต โ (๐ด ยทo (ฯ
โo ๐ต)) =
(ฯ โo ๐ต)))) |
154 | 153 | com12 32 |
. . . . 5
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง ฯ
โ On) โ (๐ต โ
On โ (โ
โ ๐ต
โ (๐ด
ยทo (ฯ โo ๐ต)) = (ฯ โo ๐ต)))) |
155 | 154 | adantrr 716 |
. . . 4
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ต โ
On)) โ (๐ต โ On
โ (โ
โ ๐ต
โ (๐ด
ยทo (ฯ โo ๐ต)) = (ฯ โo ๐ต)))) |
156 | 155 | imp32 420 |
. . 3
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (ฯ
โ On โง ๐ต โ
On)) โง (๐ต โ On
โง โ
โ ๐ต))
โ (๐ด
ยทo (ฯ โo ๐ต)) = (ฯ โo ๐ต)) |
157 | 156 | an32s 651 |
. 2
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โง (ฯ โ
On โง ๐ต โ On))
โ (๐ด
ยทo (ฯ โo ๐ต)) = (ฯ โo ๐ต)) |
158 | | nnm0 8605 |
. . . 4
โข (๐ด โ ฯ โ (๐ด ยทo โ
) =
โ
) |
159 | 158 | ad3antrrr 729 |
. . 3
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โง ยฌ (ฯ
โ On โง ๐ต โ
On)) โ (๐ด
ยทo โ
) = โ
) |
160 | | fnoe 8510 |
. . . . . . 7
โข
โo Fn (On ร On) |
161 | | fndm 6653 |
. . . . . . 7
โข (
โo Fn (On ร On) โ dom โo = (On
ร On)) |
162 | 160, 161 | ax-mp 5 |
. . . . . 6
โข dom
โo = (On ร On) |
163 | 162 | ndmov 7591 |
. . . . 5
โข (ยฌ
(ฯ โ On โง ๐ต
โ On) โ (ฯ โo ๐ต) = โ
) |
164 | 163 | adantl 483 |
. . . 4
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โง ยฌ (ฯ
โ On โง ๐ต โ
On)) โ (ฯ โo ๐ต) = โ
) |
165 | 164 | oveq2d 7425 |
. . 3
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โง ยฌ (ฯ
โ On โง ๐ต โ
On)) โ (๐ด
ยทo (ฯ โo ๐ต)) = (๐ด ยทo
โ
)) |
166 | 159, 165,
164 | 3eqtr4d 2783 |
. 2
โข ((((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โง ยฌ (ฯ
โ On โง ๐ต โ
On)) โ (๐ด
ยทo (ฯ โo ๐ต)) = (ฯ โo ๐ต)) |
167 | 157, 166 | pm2.61dan 812 |
1
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง (๐ต โ On โง โ
โ
๐ต)) โ (๐ด ยทo (ฯ
โo ๐ต)) =
(ฯ โo ๐ต)) |