Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . 3
โข (๐ฅ = โ
โ (1o
โo ๐ฅ) =
(1o โo โ
)) |
2 | 1 | eqeq1d 2735 |
. 2
โข (๐ฅ = โ
โ
((1o โo ๐ฅ) = 1o โ (1o
โo โ
) = 1o)) |
3 | | oveq2 7369 |
. . 3
โข (๐ฅ = ๐ฆ โ (1o โo
๐ฅ) = (1o
โo ๐ฆ)) |
4 | 3 | eqeq1d 2735 |
. 2
โข (๐ฅ = ๐ฆ โ ((1o โo
๐ฅ) = 1o โ
(1o โo ๐ฆ) = 1o)) |
5 | | oveq2 7369 |
. . 3
โข (๐ฅ = suc ๐ฆ โ (1o โo
๐ฅ) = (1o
โo suc ๐ฆ)) |
6 | 5 | eqeq1d 2735 |
. 2
โข (๐ฅ = suc ๐ฆ โ ((1o โo
๐ฅ) = 1o โ
(1o โo suc ๐ฆ) = 1o)) |
7 | | oveq2 7369 |
. . 3
โข (๐ฅ = ๐ด โ (1o โo
๐ฅ) = (1o
โo ๐ด)) |
8 | 7 | eqeq1d 2735 |
. 2
โข (๐ฅ = ๐ด โ ((1o โo
๐ฅ) = 1o โ
(1o โo ๐ด) = 1o)) |
9 | | 1on 8428 |
. . 3
โข
1o โ On |
10 | | oe0 8472 |
. . 3
โข
(1o โ On โ (1o โo
โ
) = 1o) |
11 | 9, 10 | ax-mp 5 |
. 2
โข
(1o โo โ
) =
1o |
12 | | oesuc 8477 |
. . . . 5
โข
((1o โ On โง ๐ฆ โ On) โ (1o
โo suc ๐ฆ) =
((1o โo ๐ฆ) ยทo
1o)) |
13 | 9, 12 | mpan 689 |
. . . 4
โข (๐ฆ โ On โ (1o
โo suc ๐ฆ) =
((1o โo ๐ฆ) ยทo
1o)) |
14 | | oveq1 7368 |
. . . . 5
โข
((1o โo ๐ฆ) = 1o โ ((1o
โo ๐ฆ)
ยทo 1o) = (1o ยทo
1o)) |
15 | | om1 8493 |
. . . . . 6
โข
(1o โ On โ (1o ยทo
1o) = 1o) |
16 | 9, 15 | ax-mp 5 |
. . . . 5
โข
(1o ยทo 1o) =
1o |
17 | 14, 16 | eqtrdi 2789 |
. . . 4
โข
((1o โo ๐ฆ) = 1o โ ((1o
โo ๐ฆ)
ยทo 1o) = 1o) |
18 | 13, 17 | sylan9eq 2793 |
. . 3
โข ((๐ฆ โ On โง (1o
โo ๐ฆ) =
1o) โ (1o โo suc ๐ฆ) = 1o) |
19 | 18 | ex 414 |
. 2
โข (๐ฆ โ On โ
((1o โo ๐ฆ) = 1o โ (1o
โo suc ๐ฆ) =
1o)) |
20 | | iuneq2 4977 |
. . 3
โข
(โ๐ฆ โ
๐ฅ (1o
โo ๐ฆ) =
1o โ โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ) = โช ๐ฆ โ ๐ฅ 1o) |
21 | | vex 3451 |
. . . . . 6
โข ๐ฅ โ V |
22 | | 0lt1o 8454 |
. . . . . . . 8
โข โ
โ 1o |
23 | | oelim 8484 |
. . . . . . . 8
โข
(((1o โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ 1o) โ
(1o โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ)) |
24 | 22, 23 | mpan2 690 |
. . . . . . 7
โข
((1o โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (1o โo
๐ฅ) = โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ)) |
25 | 9, 24 | mpan 689 |
. . . . . 6
โข ((๐ฅ โ V โง Lim ๐ฅ) โ (1o
โo ๐ฅ) =
โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ)) |
26 | 21, 25 | mpan 689 |
. . . . 5
โข (Lim
๐ฅ โ (1o
โo ๐ฅ) =
โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ)) |
27 | 26 | eqeq1d 2735 |
. . . 4
โข (Lim
๐ฅ โ ((1o
โo ๐ฅ) =
1o โ โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ) =
1o)) |
28 | | 0ellim 6384 |
. . . . . 6
โข (Lim
๐ฅ โ โ
โ
๐ฅ) |
29 | | ne0i 4298 |
. . . . . 6
โข (โ
โ ๐ฅ โ ๐ฅ โ โ
) |
30 | | iunconst 4967 |
. . . . . 6
โข (๐ฅ โ โ
โ โช ๐ฆ โ ๐ฅ 1o =
1o) |
31 | 28, 29, 30 | 3syl 18 |
. . . . 5
โข (Lim
๐ฅ โ โช ๐ฆ โ ๐ฅ 1o =
1o) |
32 | 31 | eqeq2d 2744 |
. . . 4
โข (Lim
๐ฅ โ (โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ) = โช ๐ฆ โ ๐ฅ 1o โ โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ) =
1o)) |
33 | 27, 32 | bitr4d 282 |
. . 3
โข (Lim
๐ฅ โ ((1o
โo ๐ฅ) =
1o โ โช ๐ฆ โ ๐ฅ (1o โo ๐ฆ) = โช ๐ฆ โ ๐ฅ 1o)) |
34 | 20, 33 | imbitrrid 245 |
. 2
โข (Lim
๐ฅ โ (โ๐ฆ โ ๐ฅ (1o โo ๐ฆ) = 1o โ
(1o โo ๐ฅ) = 1o)) |
35 | 2, 4, 6, 8, 11, 19, 34 | tfinds 7800 |
1
โข (๐ด โ On โ (1o
โo ๐ด) =
1o) |