Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo
โ
)) |
2 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = โ
โ (๐ต ยทo ๐ฅ) = (๐ต ยทo
โ
)) |
3 | 2 | oveq2d 7377 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo
โ
))) |
4 | 1, 3 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = โ
โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo โ
) = (๐ด ยทo (๐ต ยทo
โ
)))) |
5 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
6 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ฆ)) |
7 | 6 | oveq2d 7377 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo ๐ฆ))) |
8 | 5, 7 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
9 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo suc ๐ฆ)) |
10 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = suc ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo suc ๐ฆ)) |
11 | 10 | oveq2d 7377 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo suc ๐ฆ))) |
12 | 9, 11 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))) |
13 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ถ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ถ)) |
14 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = ๐ถ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ถ)) |
15 | 14 | oveq2d 7377 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo ๐ถ))) |
16 | 13, 15 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = ๐ถ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))) |
17 | | omcl 8486 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
18 | | om0 8467 |
. . . . . . 7
โข ((๐ด ยทo ๐ต) โ On โ ((๐ด ยทo ๐ต) ยทo โ
)
= โ
) |
19 | 17, 18 | syl 17 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) ยทo โ
)
= โ
) |
20 | | om0 8467 |
. . . . . . . 8
โข (๐ต โ On โ (๐ต ยทo โ
) =
โ
) |
21 | 20 | oveq2d 7377 |
. . . . . . 7
โข (๐ต โ On โ (๐ด ยทo (๐ต ยทo โ
))
= (๐ด ยทo
โ
)) |
22 | | om0 8467 |
. . . . . . 7
โข (๐ด โ On โ (๐ด ยทo โ
) =
โ
) |
23 | 21, 22 | sylan9eqr 2795 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo (๐ต ยทo โ
))
= โ
) |
24 | 19, 23 | eqtr4d 2776 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) ยทo โ
)
= (๐ด ยทo
(๐ต ยทo
โ
))) |
25 | | oveq1 7368 |
. . . . . . . . 9
โข (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
26 | | omsuc 8476 |
. . . . . . . . . . 11
โข (((๐ด ยทo ๐ต) โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต))) |
27 | 17, 26 | stoic3 1779 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต))) |
28 | | omsuc 8476 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
29 | 28 | 3adant1 1131 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
30 | 29 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo (๐ต ยทo suc ๐ฆ)) = (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต))) |
31 | | omcl 8486 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo ๐ฆ) โ On) |
32 | | odi 8530 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ On โง (๐ต ยทo ๐ฆ) โ On โง ๐ต โ On) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
33 | 31, 32 | syl3an2 1165 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ On โง (๐ต โ On โง ๐ฆ โ On) โง ๐ต โ On) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
34 | 33 | 3exp 1120 |
. . . . . . . . . . . . . . 15
โข (๐ด โ On โ ((๐ต โ On โง ๐ฆ โ On) โ (๐ต โ On โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))))) |
35 | 34 | expd 417 |
. . . . . . . . . . . . . 14
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ต โ On โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))))) |
36 | 35 | com34 91 |
. . . . . . . . . . . . 13
โข (๐ด โ On โ (๐ต โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))))) |
37 | 36 | pm2.43d 53 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))))) |
38 | 37 | 3imp 1112 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
39 | 30, 38 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo (๐ต ยทo suc ๐ฆ)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
40 | 27, 39 | eqeq12d 2749 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))) |
41 | 25, 40 | imbitrrid 245 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))) |
42 | 41 | 3exp 1120 |
. . . . . . 7
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))))) |
43 | 42 | com3r 87 |
. . . . . 6
โข (๐ฆ โ On โ (๐ด โ On โ (๐ต โ On โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))))) |
44 | 43 | impd 412 |
. . . . 5
โข (๐ฆ โ On โ ((๐ด โ On โง ๐ต โ On) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ))))) |
45 | 17 | ancoms 460 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง ๐ด โ On) โ (๐ด ยทo ๐ต) โ On) |
46 | | vex 3451 |
. . . . . . . . . . . . . . 15
โข ๐ฅ โ V |
47 | | omlim 8483 |
. . . . . . . . . . . . . . 15
โข (((๐ด ยทo ๐ต) โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
48 | 46, 47 | mpanr1 702 |
. . . . . . . . . . . . . 14
โข (((๐ด ยทo ๐ต) โ On โง Lim ๐ฅ) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
49 | 45, 48 | sylan 581 |
. . . . . . . . . . . . 13
โข (((๐ต โ On โง ๐ด โ On) โง Lim ๐ฅ) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
50 | 49 | an32s 651 |
. . . . . . . . . . . 12
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . 11
โข
(((((๐ต โ On
โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ
๐ต) โง โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ))) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
52 | | iuneq2 4977 |
. . . . . . . . . . . 12
โข
(โ๐ฆ โ
๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ โช
๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = โช ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
53 | | limelon 6385 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฅ โ V โง Lim ๐ฅ) โ ๐ฅ โ On) |
54 | 46, 53 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
โข (Lim
๐ฅ โ ๐ฅ โ On) |
55 | 54 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . 20
โข ((Lim
๐ฅ โง ๐ต โ On) โ (๐ฅ โ On โง ๐ต โ On)) |
56 | 55 | ancoms 460 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ On โง Lim ๐ฅ) โ (๐ฅ โ On โง ๐ต โ On)) |
57 | | omordi 8517 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฅ โ On โง ๐ต โ On) โง โ
โ
๐ต) โ (๐ฆ โ ๐ฅ โ (๐ต ยทo ๐ฆ) โ (๐ต ยทo ๐ฅ))) |
58 | 56, 57 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ (๐ฆ โ ๐ฅ โ (๐ต ยทo ๐ฆ) โ (๐ต ยทo ๐ฅ))) |
59 | | ssid 3970 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo (๐ต ยทo ๐ฆ)) |
60 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ง = (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) = (๐ด ยทo (๐ต ยทo ๐ฆ))) |
61 | 60 | sseq2d 3980 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = (๐ต ยทo ๐ฆ) โ ((๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
62 | 61 | rspcev 3583 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ต ยทo ๐ฆ) โ (๐ต ยทo ๐ฅ) โง (๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo (๐ต ยทo ๐ฆ))) โ โ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง)) |
63 | 59, 62 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต ยทo ๐ฆ) โ (๐ต ยทo ๐ฅ) โ โ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง)) |
64 | 58, 63 | syl6 35 |
. . . . . . . . . . . . . . . . 17
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ (๐ฆ โ ๐ฅ โ โ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง))) |
65 | 64 | ralrimiv 3139 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ โ๐ฆ โ ๐ฅ โ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง)) |
66 | | iunss2 5013 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ฆ โ
๐ฅ โ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo (๐ต ยทo ๐ฆ)) โ (๐ด ยทo ๐ง) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ)) โ โช ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ โช ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ)) โ โช ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
68 | 67 | adantlr 714 |
. . . . . . . . . . . . . 14
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ ๐ต) โ โช ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ)) โ โช ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
69 | | omcl 8486 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ On โง ๐ฅ โ On) โ (๐ต ยทo ๐ฅ) โ On) |
70 | 54, 69 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ On โง Lim ๐ฅ) โ (๐ต ยทo ๐ฅ) โ On) |
71 | | onelon 6346 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ต ยทo ๐ฅ) โ On โง ๐ง โ (๐ต ยทo ๐ฅ)) โ ๐ง โ On) |
72 | 70, 71 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ง โ (๐ต ยทo ๐ฅ)) โ ๐ง โ On) |
73 | 72 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง ๐ง โ (๐ต ยทo ๐ฅ)) โ ๐ง โ On) |
74 | | omordlim 8528 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง ๐ง โ (๐ต ยทo ๐ฅ)) โ โ๐ฆ โ ๐ฅ ๐ง โ (๐ต ยทo ๐ฆ)) |
75 | 74 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ง โ (๐ต ยทo ๐ฅ) โ โ๐ฆ โ ๐ฅ ๐ง โ (๐ต ยทo ๐ฆ))) |
76 | 46, 75 | mpanr1 702 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ต โ On โง Lim ๐ฅ) โ (๐ง โ (๐ต ยทo ๐ฅ) โ โ๐ฆ โ ๐ฅ ๐ง โ (๐ต ยทo ๐ฆ))) |
77 | 76 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โง ๐ด โ On) โ (๐ง โ (๐ต ยทo ๐ฅ) โ โ๐ฆ โ ๐ฅ ๐ง โ (๐ต ยทo ๐ฆ))) |
78 | | onelon 6346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ฅ โ On โง ๐ฆ โ ๐ฅ) โ ๐ฆ โ On) |
79 | 54, 78 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((Lim
๐ฅ โง ๐ฆ โ ๐ฅ) โ ๐ฆ โ On) |
80 | 79, 31 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ต โ On โง (Lim ๐ฅ โง ๐ฆ โ ๐ฅ)) โ (๐ต ยทo ๐ฆ) โ On) |
81 | | onelss 6363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ต ยทo ๐ฆ) โ On โ (๐ง โ (๐ต ยทo ๐ฆ) โ ๐ง โ (๐ต ยทo ๐ฆ))) |
82 | 81 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ง โ On โง (๐ต ยทo ๐ฆ) โ On โง ๐ด โ On) โ (๐ง โ (๐ต ยทo ๐ฆ) โ ๐ง โ (๐ต ยทo ๐ฆ))) |
83 | | omwordi 8522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ง โ On โง (๐ต ยทo ๐ฆ) โ On โง ๐ด โ On) โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
84 | 82, 83 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ง โ On โง (๐ต ยทo ๐ฆ) โ On โง ๐ด โ On) โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
85 | 84 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ง โ On โ ((๐ต ยทo ๐ฆ) โ On โ (๐ด โ On โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))) |
86 | 80, 85 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ง โ On โ ((๐ต โ On โง (Lim ๐ฅ โง ๐ฆ โ ๐ฅ)) โ (๐ด โ On โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))) |
87 | 86 | exp4d 435 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ง โ On โ (๐ต โ On โ (Lim ๐ฅ โ (๐ฆ โ ๐ฅ โ (๐ด โ On โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))))) |
88 | 87 | imp32 420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โ (๐ฆ โ ๐ฅ โ (๐ด โ On โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))) |
89 | 88 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โ (๐ด โ On โ (๐ฆ โ ๐ฅ โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))) |
90 | 89 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โง ๐ด โ On) โ (๐ฆ โ ๐ฅ โ (๐ง โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ))))) |
91 | 90 | reximdvai 3159 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โง ๐ด โ On) โ (โ๐ฆ โ ๐ฅ ๐ง โ (๐ต ยทo ๐ฆ) โ โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
92 | 77, 91 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ง โ On โง (๐ต โ On โง Lim ๐ฅ)) โง ๐ด โ On) โ (๐ง โ (๐ต ยทo ๐ฅ) โ โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
93 | 92 | exp31 421 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง โ On โ ((๐ต โ On โง Lim ๐ฅ) โ (๐ด โ On โ (๐ง โ (๐ต ยทo ๐ฅ) โ โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))))) |
94 | 93 | imp4c 425 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง โ On โ ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง ๐ง โ (๐ต ยทo ๐ฅ)) โ โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
95 | 73, 94 | mpcom 38 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง ๐ง โ (๐ต ยทo ๐ฅ)) โ โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
96 | 95 | ralrimiva 3140 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ โ๐ง โ (๐ต ยทo ๐ฅ)โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
97 | | iunss2 5013 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ง โ
(๐ต ยทo
๐ฅ)โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ง) โ (๐ด ยทo (๐ต ยทo ๐ฆ)) โ โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ โช ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
99 | 98 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ ๐ต) โ โช ๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ))) |
100 | 68, 99 | eqssd 3965 |
. . . . . . . . . . . . 13
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ ๐ต) โ โช ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
101 | | omlimcl 8529 |
. . . . . . . . . . . . . . . . 17
โข (((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ต) โ Lim (๐ต ยทo ๐ฅ)) |
102 | 46, 101 | mpanlr1 705 |
. . . . . . . . . . . . . . . 16
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ Lim (๐ต ยทo ๐ฅ)) |
103 | | ovex 7394 |
. . . . . . . . . . . . . . . . 17
โข (๐ต ยทo ๐ฅ) โ V |
104 | | omlim 8483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ On โง ((๐ต ยทo ๐ฅ) โ V โง Lim (๐ต ยทo ๐ฅ))) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
105 | 103, 104 | mpanr1 702 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ On โง Lim (๐ต ยทo ๐ฅ)) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
106 | 102, 105 | sylan2 594 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ On โง ((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต)) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
107 | 106 | ancoms 460 |
. . . . . . . . . . . . . 14
โข ((((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โง ๐ด โ On) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
108 | 107 | an32s 651 |
. . . . . . . . . . . . 13
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ ๐ต) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โช
๐ง โ (๐ต ยทo ๐ฅ)(๐ด ยทo ๐ง)) |
109 | 100, 108 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข ((((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ ๐ต) โ โช ๐ฆ โ ๐ฅ (๐ด ยทo (๐ต ยทo ๐ฆ)) = (๐ด ยทo (๐ต ยทo ๐ฅ))) |
110 | 52, 109 | sylan9eqr 2795 |
. . . . . . . . . . 11
โข
(((((๐ต โ On
โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ
๐ต) โง โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ))) โ โช ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฅ))) |
111 | 51, 110 | eqtrd 2773 |
. . . . . . . . . 10
โข
(((((๐ต โ On
โง Lim ๐ฅ) โง ๐ด โ On) โง โ
โ
๐ต) โง โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ))) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))) |
112 | 111 | exp31 421 |
. . . . . . . . 9
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (โ
โ ๐ต โ (โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))))) |
113 | | eloni 6331 |
. . . . . . . . . . . . 13
โข (๐ต โ On โ Ord ๐ต) |
114 | | ord0eln0 6376 |
. . . . . . . . . . . . . 14
โข (Ord
๐ต โ (โ
โ
๐ต โ ๐ต โ โ
)) |
115 | 114 | necon2bbid 2984 |
. . . . . . . . . . . . 13
โข (Ord
๐ต โ (๐ต = โ
โ ยฌ โ
โ ๐ต)) |
116 | 113, 115 | syl 17 |
. . . . . . . . . . . 12
โข (๐ต โ On โ (๐ต = โ
โ ยฌ โ
โ ๐ต)) |
117 | 116 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (๐ต = โ
โ ยฌ โ
โ ๐ต)) |
118 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ต = โ
โ (๐ด ยทo ๐ต) = (๐ด ยทo
โ
)) |
119 | 118, 22 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ On โง ๐ต = โ
) โ (๐ด ยทo ๐ต) = โ
) |
120 | 119 | oveq1d 7376 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ On โง ๐ต = โ
) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (โ
ยทo ๐ฅ)) |
121 | | om0r 8489 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ On โ (โ
ยทo ๐ฅ) =
โ
) |
122 | 120, 121 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ On โง (๐ด โ On โง ๐ต = โ
)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โ
) |
123 | 122 | anassrs 469 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ On โง ๐ด โ On) โง ๐ต = โ
) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = โ
) |
124 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ต = โ
โ (๐ต ยทo ๐ฅ) = (โ
ยทo ๐ฅ)) |
125 | 124, 121 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ On โง ๐ต = โ
) โ (๐ต ยทo ๐ฅ) = โ
) |
126 | 125 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ On โง ๐ต = โ
) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo
โ
)) |
127 | 126, 22 | sylan9eq 2793 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ On โง ๐ต = โ
) โง ๐ด โ On) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โ
) |
128 | 127 | an32s 651 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ On โง ๐ด โ On) โง ๐ต = โ
) โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = โ
) |
129 | 123, 128 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ On โง ๐ด โ On) โง ๐ต = โ
) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))) |
130 | 129 | ex 414 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ On โง ๐ด โ On) โ (๐ต = โ
โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
131 | 54, 130 | sylan 581 |
. . . . . . . . . . . 12
โข ((Lim
๐ฅ โง ๐ด โ On) โ (๐ต = โ
โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
132 | 131 | adantll 713 |
. . . . . . . . . . 11
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (๐ต = โ
โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
133 | 117, 132 | sylbird 260 |
. . . . . . . . . 10
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (ยฌ โ
โ
๐ต โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
134 | 133 | a1dd 50 |
. . . . . . . . 9
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (ยฌ โ
โ
๐ต โ (โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))))) |
135 | 112, 134 | pm2.61d 179 |
. . . . . . . 8
โข (((๐ต โ On โง Lim ๐ฅ) โง ๐ด โ On) โ (โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
136 | 135 | exp31 421 |
. . . . . . 7
โข (๐ต โ On โ (Lim ๐ฅ โ (๐ด โ On โ (โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))))) |
137 | 136 | com3l 89 |
. . . . . 6
โข (Lim
๐ฅ โ (๐ด โ On โ (๐ต โ On โ (โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))))) |
138 | 137 | impd 412 |
. . . . 5
โข (Lim
๐ฅ โ ((๐ด โ On โง ๐ต โ On) โ
(โ๐ฆ โ ๐ฅ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))))) |
139 | 4, 8, 12, 16, 24, 44, 138 | tfinds3 7805 |
. . . 4
โข (๐ถ โ On โ ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))) |
140 | 139 | expd 417 |
. . 3
โข (๐ถ โ On โ (๐ด โ On โ (๐ต โ On โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))) |
141 | 140 | com3l 89 |
. 2
โข (๐ด โ On โ (๐ต โ On โ (๐ถ โ On โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))) |
142 | 141 | 3imp 1112 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))) |