Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . 3
โข (๐ฅ = โ
โ (1o
ยทo ๐ฅ) =
(1o ยทo โ
)) |
2 | | id 22 |
. . 3
โข (๐ฅ = โ
โ ๐ฅ = โ
) |
3 | 1, 2 | eqeq12d 2749 |
. 2
โข (๐ฅ = โ
โ
((1o ยทo ๐ฅ) = ๐ฅ โ (1o ยทo
โ
) = โ
)) |
4 | | oveq2 7369 |
. . 3
โข (๐ฅ = ๐ฆ โ (1o ยทo
๐ฅ) = (1o
ยทo ๐ฆ)) |
5 | | id 22 |
. . 3
โข (๐ฅ = ๐ฆ โ ๐ฅ = ๐ฆ) |
6 | 4, 5 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ฆ โ ((1o ยทo
๐ฅ) = ๐ฅ โ (1o ยทo
๐ฆ) = ๐ฆ)) |
7 | | oveq2 7369 |
. . 3
โข (๐ฅ = suc ๐ฆ โ (1o ยทo
๐ฅ) = (1o
ยทo suc ๐ฆ)) |
8 | | id 22 |
. . 3
โข (๐ฅ = suc ๐ฆ โ ๐ฅ = suc ๐ฆ) |
9 | 7, 8 | eqeq12d 2749 |
. 2
โข (๐ฅ = suc ๐ฆ โ ((1o ยทo
๐ฅ) = ๐ฅ โ (1o ยทo
suc ๐ฆ) = suc ๐ฆ)) |
10 | | oveq2 7369 |
. . 3
โข (๐ฅ = ๐ด โ (1o ยทo
๐ฅ) = (1o
ยทo ๐ด)) |
11 | | id 22 |
. . 3
โข (๐ฅ = ๐ด โ ๐ฅ = ๐ด) |
12 | 10, 11 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ด โ ((1o ยทo
๐ฅ) = ๐ฅ โ (1o ยทo
๐ด) = ๐ด)) |
13 | | 1on 8428 |
. . 3
โข
1o โ On |
14 | | om0 8467 |
. . 3
โข
(1o โ On โ (1o ยทo
โ
) = โ
) |
15 | 13, 14 | ax-mp 5 |
. 2
โข
(1o ยทo โ
) = โ
|
16 | | omsuc 8476 |
. . . . . 6
โข
((1o โ On โง ๐ฆ โ On) โ (1o
ยทo suc ๐ฆ)
= ((1o ยทo ๐ฆ) +o
1o)) |
17 | 13, 16 | mpan 689 |
. . . . 5
โข (๐ฆ โ On โ (1o
ยทo suc ๐ฆ)
= ((1o ยทo ๐ฆ) +o
1o)) |
18 | | oveq1 7368 |
. . . . 5
โข
((1o ยทo ๐ฆ) = ๐ฆ โ ((1o ยทo
๐ฆ) +o
1o) = (๐ฆ
+o 1o)) |
19 | 17, 18 | sylan9eq 2793 |
. . . 4
โข ((๐ฆ โ On โง (1o
ยทo ๐ฆ) =
๐ฆ) โ (1o
ยทo suc ๐ฆ)
= (๐ฆ +o
1o)) |
20 | | oa1suc 8481 |
. . . . 5
โข (๐ฆ โ On โ (๐ฆ +o 1o) =
suc ๐ฆ) |
21 | 20 | adantr 482 |
. . . 4
โข ((๐ฆ โ On โง (1o
ยทo ๐ฆ) =
๐ฆ) โ (๐ฆ +o 1o) =
suc ๐ฆ) |
22 | 19, 21 | eqtrd 2773 |
. . 3
โข ((๐ฆ โ On โง (1o
ยทo ๐ฆ) =
๐ฆ) โ (1o
ยทo suc ๐ฆ)
= suc ๐ฆ) |
23 | 22 | ex 414 |
. 2
โข (๐ฆ โ On โ
((1o ยทo ๐ฆ) = ๐ฆ โ (1o ยทo
suc ๐ฆ) = suc ๐ฆ)) |
24 | | iuneq2 4977 |
. . . 4
โข
(โ๐ฆ โ
๐ฅ (1o
ยทo ๐ฆ) =
๐ฆ โ โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ) = โช ๐ฆ โ ๐ฅ ๐ฆ) |
25 | | uniiun 5022 |
. . . 4
โข โช ๐ฅ =
โช ๐ฆ โ ๐ฅ ๐ฆ |
26 | 24, 25 | eqtr4di 2791 |
. . 3
โข
(โ๐ฆ โ
๐ฅ (1o
ยทo ๐ฆ) =
๐ฆ โ โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ) = โช
๐ฅ) |
27 | | vex 3451 |
. . . . 5
โข ๐ฅ โ V |
28 | | omlim 8483 |
. . . . . 6
โข
((1o โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (1o ยทo
๐ฅ) = โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ)) |
29 | 13, 28 | mpan 689 |
. . . . 5
โข ((๐ฅ โ V โง Lim ๐ฅ) โ (1o
ยทo ๐ฅ) =
โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ)) |
30 | 27, 29 | mpan 689 |
. . . 4
โข (Lim
๐ฅ โ (1o
ยทo ๐ฅ) =
โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ)) |
31 | | limuni 6382 |
. . . 4
โข (Lim
๐ฅ โ ๐ฅ = โช ๐ฅ) |
32 | 30, 31 | eqeq12d 2749 |
. . 3
โข (Lim
๐ฅ โ ((1o
ยทo ๐ฅ) =
๐ฅ โ โช ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ) = โช
๐ฅ)) |
33 | 26, 32 | imbitrrid 245 |
. 2
โข (Lim
๐ฅ โ (โ๐ฆ โ ๐ฅ (1o ยทo ๐ฆ) = ๐ฆ โ (1o ยทo
๐ฅ) = ๐ฅ)) |
34 | 3, 6, 9, 12, 15, 23, 33 | tfinds 7800 |
1
โข (๐ด โ On โ (1o
ยทo ๐ด) =
๐ด) |