Step | Hyp | Ref
| Expression |
1 | | df-suc 4371 |
. . . . . . 7
โข suc ๐ต = (๐ต โช {๐ต}) |
2 | | iuneq1 3899 |
. . . . . . 7
โข (suc
๐ต = (๐ต โช {๐ต}) โ โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด) = โช
๐ฅ โ (๐ต โช {๐ต})((๐ด ยทo ๐ฅ) +o ๐ด)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
โข โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด) = โช
๐ฅ โ (๐ต โช {๐ต})((๐ด ยทo ๐ฅ) +o ๐ด) |
4 | | iunxun 3966 |
. . . . . 6
โข โช ๐ฅ โ (๐ต โช {๐ต})((๐ด ยทo ๐ฅ) +o ๐ด) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช โช
๐ฅ โ {๐ต} ((๐ด ยทo ๐ฅ) +o ๐ด)) |
5 | 3, 4 | eqtri 2198 |
. . . . 5
โข โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช โช
๐ฅ โ {๐ต} ((๐ด ยทo ๐ฅ) +o ๐ด)) |
6 | | oveq2 5882 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ต)) |
7 | 6 | oveq1d 5889 |
. . . . . . 7
โข (๐ฅ = ๐ต โ ((๐ด ยทo ๐ฅ) +o ๐ด) = ((๐ด ยทo ๐ต) +o ๐ด)) |
8 | 7 | iunxsng 3962 |
. . . . . 6
โข (๐ต โ On โ โช ๐ฅ โ {๐ต} ((๐ด ยทo ๐ฅ) +o ๐ด) = ((๐ด ยทo ๐ต) +o ๐ด)) |
9 | 8 | uneq2d 3289 |
. . . . 5
โข (๐ต โ On โ (โช ๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช โช
๐ฅ โ {๐ต} ((๐ด ยทo ๐ฅ) +o ๐ด)) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช ((๐ด ยทo ๐ต) +o ๐ด))) |
10 | 5, 9 | eqtrid 2222 |
. . . 4
โข (๐ต โ On โ โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช ((๐ด ยทo ๐ต) +o ๐ด))) |
11 | 10 | adantl 277 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช ((๐ด ยทo ๐ต) +o ๐ด))) |
12 | | onsuc 4500 |
. . . 4
โข (๐ต โ On โ suc ๐ต โ On) |
13 | | omv2 6465 |
. . . 4
โข ((๐ด โ On โง suc ๐ต โ On) โ (๐ด ยทo suc ๐ต) = โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด)) |
14 | 12, 13 | sylan2 286 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo suc ๐ต) = โช ๐ฅ โ suc ๐ต((๐ด ยทo ๐ฅ) +o ๐ด)) |
15 | | omv2 6465 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) = โช ๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด)) |
16 | 15 | uneq1d 3288 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) โช ((๐ด ยทo ๐ต) +o ๐ด)) = (โช
๐ฅ โ ๐ต ((๐ด ยทo ๐ฅ) +o ๐ด) โช ((๐ด ยทo ๐ต) +o ๐ด))) |
17 | 11, 14, 16 | 3eqtr4d 2220 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo suc ๐ต) = ((๐ด ยทo ๐ต) โช ((๐ด ยทo ๐ต) +o ๐ด))) |
18 | | omcl 6461 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
19 | | simpl 109 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ๐ด โ On) |
20 | | oaword1 6471 |
. . . 4
โข (((๐ด ยทo ๐ต) โ On โง ๐ด โ On) โ (๐ด ยทo ๐ต) โ ((๐ด ยทo ๐ต) +o ๐ด)) |
21 | | ssequn1 3305 |
. . . 4
โข ((๐ด ยทo ๐ต) โ ((๐ด ยทo ๐ต) +o ๐ด) โ ((๐ด ยทo ๐ต) โช ((๐ด ยทo ๐ต) +o ๐ด)) = ((๐ด ยทo ๐ต) +o ๐ด)) |
22 | 20, 21 | sylib 122 |
. . 3
โข (((๐ด ยทo ๐ต) โ On โง ๐ด โ On) โ ((๐ด ยทo ๐ต) โช ((๐ด ยทo ๐ต) +o ๐ด)) = ((๐ด ยทo ๐ต) +o ๐ด)) |
23 | 18, 19, 22 | syl2anc 411 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) โช ((๐ด ยทo ๐ต) +o ๐ด)) = ((๐ด ยทo ๐ต) +o ๐ด)) |
24 | 17, 23 | eqtrd 2210 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo suc ๐ต) = ((๐ด ยทo ๐ต) +o ๐ด)) |