Step | Hyp | Ref
| Expression |
1 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = ๐ต โ (๐ด โo ๐ฅ) = (๐ด โo ๐ต)) |
2 | 1 | eleq1d 2817 |
. . . 4
โข (๐ฅ = ๐ต โ ((๐ด โo ๐ฅ) โ ฯ โ (๐ด โo ๐ต) โ ฯ)) |
3 | 2 | imbi2d 340 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ด โ ฯ โ (๐ด โo ๐ฅ) โ ฯ) โ (๐ด โ ฯ โ (๐ด โo ๐ต) โ ฯ))) |
4 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = โ
โ (๐ด โo ๐ฅ) = (๐ด โo
โ
)) |
5 | 4 | eleq1d 2817 |
. . . 4
โข (๐ฅ = โ
โ ((๐ด โo ๐ฅ) โ ฯ โ (๐ด โo โ
)
โ ฯ)) |
6 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ฆ)) |
7 | 6 | eleq1d 2817 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด โo ๐ฅ) โ ฯ โ (๐ด โo ๐ฆ) โ ฯ)) |
8 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo suc ๐ฆ)) |
9 | 8 | eleq1d 2817 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ ((๐ด โo ๐ฅ) โ ฯ โ (๐ด โo suc ๐ฆ) โ ฯ)) |
10 | | nnon 7865 |
. . . . . 6
โข (๐ด โ ฯ โ ๐ด โ On) |
11 | | oe0 8528 |
. . . . . 6
โข (๐ด โ On โ (๐ด โo โ
) =
1o) |
12 | 10, 11 | syl 17 |
. . . . 5
โข (๐ด โ ฯ โ (๐ด โo โ
) =
1o) |
13 | | df-1o 8472 |
. . . . . 6
โข
1o = suc โ
|
14 | | peano1 7883 |
. . . . . . 7
โข โ
โ ฯ |
15 | | peano2 7885 |
. . . . . . 7
โข (โ
โ ฯ โ suc โ
โ ฯ) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
โข suc
โ
โ ฯ |
17 | 13, 16 | eqeltri 2828 |
. . . . 5
โข
1o โ ฯ |
18 | 12, 17 | eqeltrdi 2840 |
. . . 4
โข (๐ด โ ฯ โ (๐ด โo โ
)
โ ฯ) |
19 | | nnmcl 8618 |
. . . . . . . 8
โข (((๐ด โo ๐ฆ) โ ฯ โง ๐ด โ ฯ) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ
ฯ) |
20 | 19 | expcom 413 |
. . . . . . 7
โข (๐ด โ ฯ โ ((๐ด โo ๐ฆ) โ ฯ โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ
ฯ)) |
21 | 20 | adantr 480 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด โo ๐ฆ) โ ฯ โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ
ฯ)) |
22 | | nnesuc 8614 |
. . . . . . 7
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
23 | 22 | eleq1d 2817 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด โo suc ๐ฆ) โ ฯ โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ
ฯ)) |
24 | 21, 23 | sylibrd 259 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด โo ๐ฆ) โ ฯ โ (๐ด โo suc ๐ฆ) โ
ฯ)) |
25 | 24 | expcom 413 |
. . . 4
โข (๐ฆ โ ฯ โ (๐ด โ ฯ โ ((๐ด โo ๐ฆ) โ ฯ โ (๐ด โo suc ๐ฆ) โ
ฯ))) |
26 | 5, 7, 9, 18, 25 | finds2 7895 |
. . 3
โข (๐ฅ โ ฯ โ (๐ด โ ฯ โ (๐ด โo ๐ฅ) โ
ฯ)) |
27 | 3, 26 | vtoclga 3566 |
. 2
โข (๐ต โ ฯ โ (๐ด โ ฯ โ (๐ด โo ๐ต) โ
ฯ)) |
28 | 27 | impcom 407 |
1
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด โo ๐ต) โ
ฯ) |