Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
โข ( ๐ฅ = โ
โ ( 1o ยทo ๐ฅ ) = ( 1o ยทo โ
) ) |
2 |
|
id |
โข ( ๐ฅ = โ
โ ๐ฅ = โ
) |
3 |
1 2
|
eqeq12d |
โข ( ๐ฅ = โ
โ ( ( 1o ยทo ๐ฅ ) = ๐ฅ โ ( 1o ยทo โ
) = โ
) ) |
4 |
|
oveq2 |
โข ( ๐ฅ = ๐ฆ โ ( 1o ยทo ๐ฅ ) = ( 1o ยทo ๐ฆ ) ) |
5 |
|
id |
โข ( ๐ฅ = ๐ฆ โ ๐ฅ = ๐ฆ ) |
6 |
4 5
|
eqeq12d |
โข ( ๐ฅ = ๐ฆ โ ( ( 1o ยทo ๐ฅ ) = ๐ฅ โ ( 1o ยทo ๐ฆ ) = ๐ฆ ) ) |
7 |
|
oveq2 |
โข ( ๐ฅ = suc ๐ฆ โ ( 1o ยทo ๐ฅ ) = ( 1o ยทo suc ๐ฆ ) ) |
8 |
|
id |
โข ( ๐ฅ = suc ๐ฆ โ ๐ฅ = suc ๐ฆ ) |
9 |
7 8
|
eqeq12d |
โข ( ๐ฅ = suc ๐ฆ โ ( ( 1o ยทo ๐ฅ ) = ๐ฅ โ ( 1o ยทo suc ๐ฆ ) = suc ๐ฆ ) ) |
10 |
|
oveq2 |
โข ( ๐ฅ = ๐ด โ ( 1o ยทo ๐ฅ ) = ( 1o ยทo ๐ด ) ) |
11 |
|
id |
โข ( ๐ฅ = ๐ด โ ๐ฅ = ๐ด ) |
12 |
10 11
|
eqeq12d |
โข ( ๐ฅ = ๐ด โ ( ( 1o ยทo ๐ฅ ) = ๐ฅ โ ( 1o ยทo ๐ด ) = ๐ด ) ) |
13 |
|
1on |
โข 1o โ On |
14 |
|
om0 |
โข ( 1o โ On โ ( 1o ยทo โ
) = โ
) |
15 |
13 14
|
ax-mp |
โข ( 1o ยทo โ
) = โ
|
16 |
|
omsuc |
โข ( ( 1o โ On โง ๐ฆ โ On ) โ ( 1o ยทo suc ๐ฆ ) = ( ( 1o ยทo ๐ฆ ) +o 1o ) ) |
17 |
13 16
|
mpan |
โข ( ๐ฆ โ On โ ( 1o ยทo suc ๐ฆ ) = ( ( 1o ยทo ๐ฆ ) +o 1o ) ) |
18 |
|
oveq1 |
โข ( ( 1o ยทo ๐ฆ ) = ๐ฆ โ ( ( 1o ยทo ๐ฆ ) +o 1o ) = ( ๐ฆ +o 1o ) ) |
19 |
17 18
|
sylan9eq |
โข ( ( ๐ฆ โ On โง ( 1o ยทo ๐ฆ ) = ๐ฆ ) โ ( 1o ยทo suc ๐ฆ ) = ( ๐ฆ +o 1o ) ) |
20 |
|
oa1suc |
โข ( ๐ฆ โ On โ ( ๐ฆ +o 1o ) = suc ๐ฆ ) |
21 |
20
|
adantr |
โข ( ( ๐ฆ โ On โง ( 1o ยทo ๐ฆ ) = ๐ฆ ) โ ( ๐ฆ +o 1o ) = suc ๐ฆ ) |
22 |
19 21
|
eqtrd |
โข ( ( ๐ฆ โ On โง ( 1o ยทo ๐ฆ ) = ๐ฆ ) โ ( 1o ยทo suc ๐ฆ ) = suc ๐ฆ ) |
23 |
22
|
ex |
โข ( ๐ฆ โ On โ ( ( 1o ยทo ๐ฆ ) = ๐ฆ โ ( 1o ยทo suc ๐ฆ ) = suc ๐ฆ ) ) |
24 |
|
iuneq2 |
โข ( โ ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = ๐ฆ โ โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = โช ๐ฆ โ ๐ฅ ๐ฆ ) |
25 |
|
uniiun |
โข โช ๐ฅ = โช ๐ฆ โ ๐ฅ ๐ฆ |
26 |
24 25
|
eqtr4di |
โข ( โ ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = ๐ฆ โ โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = โช ๐ฅ ) |
27 |
|
vex |
โข ๐ฅ โ V |
28 |
|
omlim |
โข ( ( 1o โ On โง ( ๐ฅ โ V โง Lim ๐ฅ ) ) โ ( 1o ยทo ๐ฅ ) = โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) ) |
29 |
13 28
|
mpan |
โข ( ( ๐ฅ โ V โง Lim ๐ฅ ) โ ( 1o ยทo ๐ฅ ) = โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) ) |
30 |
27 29
|
mpan |
โข ( Lim ๐ฅ โ ( 1o ยทo ๐ฅ ) = โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) ) |
31 |
|
limuni |
โข ( Lim ๐ฅ โ ๐ฅ = โช ๐ฅ ) |
32 |
30 31
|
eqeq12d |
โข ( Lim ๐ฅ โ ( ( 1o ยทo ๐ฅ ) = ๐ฅ โ โช ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = โช ๐ฅ ) ) |
33 |
26 32
|
imbitrrid |
โข ( Lim ๐ฅ โ ( โ ๐ฆ โ ๐ฅ ( 1o ยทo ๐ฆ ) = ๐ฆ โ ( 1o ยทo ๐ฅ ) = ๐ฅ ) ) |
34 |
3 6 9 12 15 23 33
|
tfinds |
โข ( ๐ด โ On โ ( 1o ยทo ๐ด ) = ๐ด ) |