Step | Hyp | Ref
| Expression |
1 | | oveq1 7368 |
. . . 4
โข (๐ด = โ
โ (๐ด โo suc ๐ต) = (โ
โo
suc ๐ต)) |
2 | | oesuclem.1 |
. . . . . . . 8
โข Lim ๐ |
3 | | limord 6381 |
. . . . . . . 8
โข (Lim
๐ โ Ord ๐) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
โข Ord ๐ |
5 | | ordelord 6343 |
. . . . . . 7
โข ((Ord
๐ โง ๐ต โ ๐) โ Ord ๐ต) |
6 | 4, 5 | mpan 689 |
. . . . . 6
โข (๐ต โ ๐ โ Ord ๐ต) |
7 | | 0elsuc 7774 |
. . . . . 6
โข (Ord
๐ต โ โ
โ suc
๐ต) |
8 | 6, 7 | syl 17 |
. . . . 5
โข (๐ต โ ๐ โ โ
โ suc ๐ต) |
9 | | limsuc 7789 |
. . . . . . 7
โข (Lim
๐ โ (๐ต โ ๐ โ suc ๐ต โ ๐)) |
10 | 2, 9 | ax-mp 5 |
. . . . . 6
โข (๐ต โ ๐ โ suc ๐ต โ ๐) |
11 | | ordelon 6345 |
. . . . . . . 8
โข ((Ord
๐ โง suc ๐ต โ ๐) โ suc ๐ต โ On) |
12 | 4, 11 | mpan 689 |
. . . . . . 7
โข (suc
๐ต โ ๐ โ suc ๐ต โ On) |
13 | | oe0m1 8471 |
. . . . . . 7
โข (suc
๐ต โ On โ (โ
โ suc ๐ต โ
(โ
โo suc ๐ต) = โ
)) |
14 | 12, 13 | syl 17 |
. . . . . 6
โข (suc
๐ต โ ๐ โ (โ
โ suc ๐ต โ (โ
โo suc ๐ต) =
โ
)) |
15 | 10, 14 | sylbi 216 |
. . . . 5
โข (๐ต โ ๐ โ (โ
โ suc ๐ต โ (โ
โo suc ๐ต) =
โ
)) |
16 | 8, 15 | mpbid 231 |
. . . 4
โข (๐ต โ ๐ โ (โ
โo suc
๐ต) =
โ
) |
17 | 1, 16 | sylan9eqr 2795 |
. . 3
โข ((๐ต โ ๐ โง ๐ด = โ
) โ (๐ด โo suc ๐ต) = โ
) |
18 | | oveq1 7368 |
. . . . 5
โข (๐ด = โ
โ (๐ด โo ๐ต) = (โ
โo
๐ต)) |
19 | | id 22 |
. . . . 5
โข (๐ด = โ
โ ๐ด = โ
) |
20 | 18, 19 | oveq12d 7379 |
. . . 4
โข (๐ด = โ
โ ((๐ด โo ๐ต) ยทo ๐ด) = ((โ
โo
๐ต) ยทo
โ
)) |
21 | | ordelon 6345 |
. . . . . . 7
โข ((Ord
๐ โง ๐ต โ ๐) โ ๐ต โ On) |
22 | 4, 21 | mpan 689 |
. . . . . 6
โข (๐ต โ ๐ โ ๐ต โ On) |
23 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ต = โ
โ (โ
โo ๐ต) =
(โ
โo โ
)) |
24 | | oe0m0 8470 |
. . . . . . . . . 10
โข (โ
โo โ
) = 1o |
25 | | 1on 8428 |
. . . . . . . . . 10
โข
1o โ On |
26 | 24, 25 | eqeltri 2830 |
. . . . . . . . 9
โข (โ
โo โ
) โ On |
27 | 23, 26 | eqeltrdi 2842 |
. . . . . . . 8
โข (๐ต = โ
โ (โ
โo ๐ต)
โ On) |
28 | 27 | adantl 483 |
. . . . . . 7
โข ((๐ต โ ๐ โง ๐ต = โ
) โ (โ
โo ๐ต)
โ On) |
29 | | oe0m1 8471 |
. . . . . . . . . . 11
โข (๐ต โ On โ (โ
โ ๐ต โ (โ
โo ๐ต) =
โ
)) |
30 | 22, 29 | syl 17 |
. . . . . . . . . 10
โข (๐ต โ ๐ โ (โ
โ ๐ต โ (โ
โo ๐ต) = โ
)) |
31 | 30 | biimpa 478 |
. . . . . . . . 9
โข ((๐ต โ ๐ โง โ
โ ๐ต) โ (โ
โo ๐ต) = โ
) |
32 | | 0elon 6375 |
. . . . . . . . 9
โข โ
โ On |
33 | 31, 32 | eqeltrdi 2842 |
. . . . . . . 8
โข ((๐ต โ ๐ โง โ
โ ๐ต) โ (โ
โo ๐ต) โ On) |
34 | 33 | adantll 713 |
. . . . . . 7
โข (((๐ต โ On โง ๐ต โ ๐) โง โ
โ ๐ต) โ (โ
โo ๐ต) โ On) |
35 | 28, 34 | oe0lem 8463 |
. . . . . 6
โข ((๐ต โ On โง ๐ต โ ๐) โ (โ
โo ๐ต) โ On) |
36 | 22, 35 | mpancom 687 |
. . . . 5
โข (๐ต โ ๐ โ (โ
โo ๐ต) โ On) |
37 | | om0 8467 |
. . . . 5
โข ((โ
โo ๐ต)
โ On โ ((โ
โo ๐ต) ยทo โ
) =
โ
) |
38 | 36, 37 | syl 17 |
. . . 4
โข (๐ต โ ๐ โ ((โ
โo ๐ต) ยทo โ
)
= โ
) |
39 | 20, 38 | sylan9eqr 2795 |
. . 3
โข ((๐ต โ ๐ โง ๐ด = โ
) โ ((๐ด โo ๐ต) ยทo ๐ด) = โ
) |
40 | 17, 39 | eqtr4d 2776 |
. 2
โข ((๐ต โ ๐ โง ๐ด = โ
) โ (๐ด โo suc ๐ต) = ((๐ด โo ๐ต) ยทo ๐ด)) |
41 | | oesuclem.2 |
. . . 4
โข (๐ต โ ๐ โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โsuc ๐ต) = ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |
42 | 41 | ad2antlr 726 |
. . 3
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โsuc ๐ต) = ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |
43 | 10, 12 | sylbi 216 |
. . . 4
โข (๐ต โ ๐ โ suc ๐ต โ On) |
44 | | oevn0 8465 |
. . . 4
โข (((๐ด โ On โง suc ๐ต โ On) โง โ
โ
๐ด) โ (๐ด โo suc ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โsuc ๐ต)) |
45 | 43, 44 | sylanl2 680 |
. . 3
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ (๐ด โo suc ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โsuc ๐ต)) |
46 | | ovex 7394 |
. . . . 5
โข (๐ด โo ๐ต) โ V |
47 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = (๐ด โo ๐ต) โ (๐ฅ ยทo ๐ด) = ((๐ด โo ๐ต) ยทo ๐ด)) |
48 | | eqid 2733 |
. . . . . 6
โข (๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)) = (๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)) |
49 | | ovex 7394 |
. . . . . 6
โข ((๐ด โo ๐ต) ยทo ๐ด) โ V |
50 | 47, 48, 49 | fvmpt 6952 |
. . . . 5
โข ((๐ด โo ๐ต) โ V โ ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(๐ด โo ๐ต)) = ((๐ด โo ๐ต) ยทo ๐ด)) |
51 | 46, 50 | ax-mp 5 |
. . . 4
โข ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(๐ด โo ๐ต)) = ((๐ด โo ๐ต) ยทo ๐ด) |
52 | | oevn0 8465 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ด โo ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต)) |
53 | 22, 52 | sylanl2 680 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ (๐ด โo ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต)) |
54 | 53 | fveq2d 6850 |
. . . 4
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(๐ด โo ๐ต)) = ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |
55 | 51, 54 | eqtr3id 2787 |
. . 3
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ ((๐ด โo ๐ต) ยทo ๐ด) = ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))โ(rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |
56 | 42, 45, 55 | 3eqtr4d 2783 |
. 2
โข (((๐ด โ On โง ๐ต โ ๐) โง โ
โ ๐ด) โ (๐ด โo suc ๐ต) = ((๐ด โo ๐ต) ยทo ๐ด)) |
57 | 40, 56 | oe0lem 8463 |
1
โข ((๐ด โ On โง ๐ต โ ๐) โ (๐ด โo suc ๐ต) = ((๐ด โo ๐ต) ยทo ๐ด)) |