Step | Hyp | Ref
| Expression |
1 | | limelon 6385 |
. . 3
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ ๐ต โ On) |
2 | | simpr 486 |
. . 3
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ Lim ๐ต) |
3 | 1, 2 | jca 513 |
. 2
โข ((๐ต โ ๐ถ โง Lim ๐ต) โ (๐ต โ On โง Lim ๐ต)) |
4 | | rdglim2a 8383 |
. . . 4
โข ((๐ต โ On โง Lim ๐ต) โ (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ต) = โช ๐ฅ โ ๐ต (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
5 | 4 | ad2antlr 726 |
. . 3
โข (((๐ด โ On โง (๐ต โ On โง Lim ๐ต)) โง โ
โ ๐ด) โ (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ต) = โช ๐ฅ โ ๐ต (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
6 | | oevn0 8465 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ด โo ๐ต) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ต)) |
7 | | onelon 6346 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
8 | | oevn0 8465 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ฅ โ On) โง โ
โ
๐ด) โ (๐ด โo ๐ฅ) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
9 | 7, 8 | sylanl2 680 |
. . . . . . . . 9
โข (((๐ด โ On โง (๐ต โ On โง ๐ฅ โ ๐ต)) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
10 | 9 | exp42 437 |
. . . . . . . 8
โข (๐ด โ On โ (๐ต โ On โ (๐ฅ โ ๐ต โ (โ
โ ๐ด โ (๐ด โo ๐ฅ) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ))))) |
11 | 10 | com34 91 |
. . . . . . 7
โข (๐ด โ On โ (๐ต โ On โ (โ
โ ๐ด โ (๐ฅ โ ๐ต โ (๐ด โo ๐ฅ) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ))))) |
12 | 11 | imp41 427 |
. . . . . 6
โข ((((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โง ๐ฅ โ ๐ต) โ (๐ด โo ๐ฅ) = (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
13 | 12 | iuneq2dv 4982 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ โช ๐ฅ โ ๐ต (๐ด โo ๐ฅ) = โช ๐ฅ โ ๐ต (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ)) |
14 | 6, 13 | eqeq12d 2749 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ ((๐ด โo ๐ต) = โช ๐ฅ โ ๐ต (๐ด โo ๐ฅ) โ (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ต) = โช
๐ฅ โ ๐ต (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ))) |
15 | 14 | adantlrr 720 |
. . 3
โข (((๐ด โ On โง (๐ต โ On โง Lim ๐ต)) โง โ
โ ๐ด) โ ((๐ด โo ๐ต) = โช
๐ฅ โ ๐ต (๐ด โo ๐ฅ) โ (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ต) = โช
๐ฅ โ ๐ต (rec((๐ฆ โ V โฆ (๐ฆ ยทo ๐ด)), 1o)โ๐ฅ))) |
16 | 5, 15 | mpbird 257 |
. 2
โข (((๐ด โ On โง (๐ต โ On โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด โo ๐ต) = โช
๐ฅ โ ๐ต (๐ด โo ๐ฅ)) |
17 | 3, 16 | sylanl2 680 |
1
โข (((๐ด โ On โง (๐ต โ ๐ถ โง Lim ๐ต)) โง โ
โ ๐ด) โ (๐ด โo ๐ต) = โช
๐ฅ โ ๐ต (๐ด โo ๐ฅ)) |