Step | Hyp | Ref
| Expression |
1 | | eqeq1 2737 |
. . 3
โข (๐ฆ = ๐ด โ (๐ฆ = โ
โ ๐ด = โ
)) |
2 | | oveq2 7369 |
. . . . . 6
โข (๐ฆ = ๐ด โ (๐ฅ ยทo ๐ฆ) = (๐ฅ ยทo ๐ด)) |
3 | 2 | mpteq2dv 5211 |
. . . . 5
โข (๐ฆ = ๐ด โ (๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)) = (๐ฅ โ V โฆ (๐ฅ ยทo ๐ด))) |
4 | | rdgeq1 8361 |
. . . . 5
โข ((๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)) = (๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)) โ rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)), 1o) = rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)) |
5 | 3, 4 | syl 17 |
. . . 4
โข (๐ฆ = ๐ด โ rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)), 1o) = rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)) |
6 | 5 | fveq1d 6848 |
. . 3
โข (๐ฆ = ๐ด โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)), 1o)โ๐ง) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ง)) |
7 | 1, 6 | ifbieq2d 4516 |
. 2
โข (๐ฆ = ๐ด โ if(๐ฆ = โ
, (1o โ ๐ง), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ฆ)), 1o)โ๐ง)) = if(๐ด = โ
, (1o โ ๐ง), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ง))) |
8 | | difeq2 4080 |
. . 3
โข (๐ง = ๐ต โ (1o โ ๐ง) = (1o โ ๐ต)) |
9 | | fveq2 6846 |
. . 3
โข (๐ง = ๐ต โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ง) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต)) |
10 | 8, 9 | ifeq12d 4511 |
. 2
โข (๐ง = ๐ต โ if(๐ด = โ
, (1o โ ๐ง), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ง)) = if(๐ด = โ
, (1o โ ๐ต), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |
11 | | df-oexp 8422 |
. 2
โข
โo = (๐ฆ
โ On, ๐ง โ On
โฆ if(๐ฆ = โ
,
(1o โ ๐ง),
(rec((๐ฅ โ V โฆ
(๐ฅ ยทo
๐ฆ)),
1o)โ๐ง))) |
12 | | 1oex 8426 |
. . . 4
โข
1o โ V |
13 | 12 | difexi 5289 |
. . 3
โข
(1o โ ๐ต) โ V |
14 | | fvex 6859 |
. . 3
โข
(rec((๐ฅ โ V
โฆ (๐ฅ
ยทo ๐ด)),
1o)โ๐ต)
โ V |
15 | 13, 14 | ifex 4540 |
. 2
โข if(๐ด = โ
, (1o
โ ๐ต), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต)) โ V |
16 | 7, 10, 11, 15 | ovmpo 7519 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) = if(๐ด = โ
, (1o โ ๐ต), (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต))) |