Step | Hyp | Ref
| Expression |
1 | | peano2 7831 |
. . . . 5
โข (๐ต โ ฯ โ suc ๐ต โ
ฯ) |
2 | | nnon 7812 |
. . . . 5
โข (suc
๐ต โ ฯ โ suc
๐ต โ
On) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐ต โ ฯ โ suc ๐ต โ On) |
4 | | omv 8462 |
. . . 4
โข ((๐ด โ On โง suc ๐ต โ On) โ (๐ด ยทo suc ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
)โsuc ๐ต)) |
5 | 3, 4 | sylan2 594 |
. . 3
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด ยทo suc ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
)โsuc ๐ต)) |
6 | 1 | adantl 483 |
. . . 4
โข ((๐ด โ On โง ๐ต โ ฯ) โ suc
๐ต โ
ฯ) |
7 | 6 | fvresd 6866 |
. . 3
โข ((๐ด โ On โง ๐ต โ ฯ) โ
((rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
) โพ
ฯ)โsuc ๐ต) =
(rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
)โsuc ๐ต)) |
8 | 5, 7 | eqtr4d 2776 |
. 2
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด ยทo suc ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โsuc
๐ต)) |
9 | | ovex 7394 |
. . . . 5
โข (๐ด ยทo ๐ต) โ V |
10 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = (๐ด ยทo ๐ต) โ (๐ฅ +o ๐ด) = ((๐ด ยทo ๐ต) +o ๐ด)) |
11 | | eqid 2733 |
. . . . . 6
โข (๐ฅ โ V โฆ (๐ฅ +o ๐ด)) = (๐ฅ โ V โฆ (๐ฅ +o ๐ด)) |
12 | | ovex 7394 |
. . . . . 6
โข ((๐ด ยทo ๐ต) +o ๐ด) โ V |
13 | 10, 11, 12 | fvmpt 6952 |
. . . . 5
โข ((๐ด ยทo ๐ต) โ V โ ((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ(๐ด ยทo ๐ต)) = ((๐ด ยทo ๐ต) +o ๐ด)) |
14 | 9, 13 | ax-mp 5 |
. . . 4
โข ((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ(๐ด ยทo ๐ต)) = ((๐ด ยทo ๐ต) +o ๐ด) |
15 | | nnon 7812 |
. . . . . . 7
โข (๐ต โ ฯ โ ๐ต โ On) |
16 | | omv 8462 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
)โ๐ต)) |
17 | 15, 16 | sylan2 594 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด ยทo ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
)โ๐ต)) |
18 | | fvres 6865 |
. . . . . . 7
โข (๐ต โ ฯ โ
((rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
) โพ
ฯ)โ๐ต) =
(rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
)โ๐ต)) |
19 | 18 | adantl 483 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ ฯ) โ
((rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
) โพ
ฯ)โ๐ต) =
(rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
)โ๐ต)) |
20 | 17, 19 | eqtr4d 2776 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด ยทo ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โ๐ต)) |
21 | 20 | fveq2d 6850 |
. . . 4
โข ((๐ด โ On โง ๐ต โ ฯ) โ ((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ(๐ด ยทo ๐ต)) = ((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โ๐ต))) |
22 | 14, 21 | eqtr3id 2787 |
. . 3
โข ((๐ด โ On โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) +o ๐ด) = ((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โ๐ต))) |
23 | | frsuc 8387 |
. . . 4
โข (๐ต โ ฯ โ
((rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
) โพ
ฯ)โsuc ๐ต) =
((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โ๐ต))) |
24 | 23 | adantl 483 |
. . 3
โข ((๐ด โ On โง ๐ต โ ฯ) โ
((rec((๐ฅ โ V โฆ
(๐ฅ +o ๐ด)), โ
) โพ
ฯ)โsuc ๐ต) =
((๐ฅ โ V โฆ (๐ฅ +o ๐ด))โ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โ๐ต))) |
25 | 22, 24 | eqtr4d 2776 |
. 2
โข ((๐ด โ On โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) +o ๐ด) = ((rec((๐ฅ โ V โฆ (๐ฅ +o ๐ด)), โ
) โพ ฯ)โsuc
๐ต)) |
26 | 8, 25 | eqtr4d 2776 |
1
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด ยทo suc ๐ต) = ((๐ด ยทo ๐ต) +o ๐ด)) |