Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . 4
โข (๐ฅ = โ
โ (๐ด ยทo ๐ฅ) = (๐ด ยทo
โ
)) |
2 | 1 | eleq1d 2819 |
. . 3
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ฅ) โ On โ (๐ด ยทo โ
)
โ On)) |
3 | | oveq2 7369 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ฆ)) |
4 | 3 | eleq1d 2819 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ฅ) โ On โ (๐ด ยทo ๐ฆ) โ On)) |
5 | | oveq2 7369 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo suc ๐ฆ)) |
6 | 5 | eleq1d 2819 |
. . 3
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ฅ) โ On โ (๐ด ยทo suc ๐ฆ) โ On)) |
7 | | oveq2 7369 |
. . . 4
โข (๐ฅ = ๐ต โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ต)) |
8 | 7 | eleq1d 2819 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ด ยทo ๐ฅ) โ On โ (๐ด ยทo ๐ต) โ On)) |
9 | | om0 8467 |
. . . 4
โข (๐ด โ On โ (๐ด ยทo โ
) =
โ
) |
10 | | 0elon 6375 |
. . . 4
โข โ
โ On |
11 | 9, 10 | eqeltrdi 2842 |
. . 3
โข (๐ด โ On โ (๐ด ยทo โ
)
โ On) |
12 | | oacl 8485 |
. . . . . . 7
โข (((๐ด ยทo ๐ฆ) โ On โง ๐ด โ On) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ On) |
13 | 12 | expcom 415 |
. . . . . 6
โข (๐ด โ On โ ((๐ด ยทo ๐ฆ) โ On โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ On)) |
14 | 13 | adantr 482 |
. . . . 5
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ฆ) โ On โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ On)) |
15 | | omsuc 8476 |
. . . . . 6
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
16 | 15 | eleq1d 2819 |
. . . . 5
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด ยทo suc ๐ฆ) โ On โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ On)) |
17 | 14, 16 | sylibrd 259 |
. . . 4
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ฆ) โ On โ (๐ด ยทo suc ๐ฆ) โ On)) |
18 | 17 | expcom 415 |
. . 3
โข (๐ฆ โ On โ (๐ด โ On โ ((๐ด ยทo ๐ฆ) โ On โ (๐ด ยทo suc ๐ฆ) โ On))) |
19 | | vex 3451 |
. . . . . 6
โข ๐ฅ โ V |
20 | | iunon 8289 |
. . . . . 6
โข ((๐ฅ โ V โง โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On) โ โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On) |
21 | 19, 20 | mpan 689 |
. . . . 5
โข
(โ๐ฆ โ
๐ฅ (๐ด ยทo ๐ฆ) โ On โ โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On) |
22 | | omlim 8483 |
. . . . . . 7
โข ((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ด ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ)) |
23 | 19, 22 | mpanr1 702 |
. . . . . 6
โข ((๐ด โ On โง Lim ๐ฅ) โ (๐ด ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ)) |
24 | 23 | eleq1d 2819 |
. . . . 5
โข ((๐ด โ On โง Lim ๐ฅ) โ ((๐ด ยทo ๐ฅ) โ On โ โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On)) |
25 | 21, 24 | imbitrrid 245 |
. . . 4
โข ((๐ด โ On โง Lim ๐ฅ) โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On โ (๐ด ยทo ๐ฅ) โ On)) |
26 | 25 | expcom 415 |
. . 3
โข (Lim
๐ฅ โ (๐ด โ On โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ On โ (๐ด ยทo ๐ฅ) โ On))) |
27 | 2, 4, 6, 8, 11, 18, 26 | tfinds3 7805 |
. 2
โข (๐ต โ On โ (๐ด โ On โ (๐ด ยทo ๐ต) โ On)) |
28 | 27 | impcom 409 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |