Step | Hyp | Ref
| Expression |
1 | | fin1a2lem.b |
. . 3
โข ๐ธ = (๐ฅ โ ฯ โฆ (2o
ยทo ๐ฅ)) |
2 | | 2onn 8644 |
. . . 4
โข
2o โ ฯ |
3 | | nnmcl 8615 |
. . . 4
โข
((2o โ ฯ โง ๐ฅ โ ฯ) โ (2o
ยทo ๐ฅ)
โ ฯ) |
4 | 2, 3 | mpan 687 |
. . 3
โข (๐ฅ โ ฯ โ
(2o ยทo ๐ฅ) โ ฯ) |
5 | 1, 4 | fmpti 7114 |
. 2
โข ๐ธ:ฯโถฯ |
6 | 1 | fin1a2lem3 10400 |
. . . . . 6
โข (๐ โ ฯ โ (๐ธโ๐) = (2o ยทo ๐)) |
7 | 1 | fin1a2lem3 10400 |
. . . . . 6
โข (๐ โ ฯ โ (๐ธโ๐) = (2o ยทo ๐)) |
8 | 6, 7 | eqeqan12d 2745 |
. . . . 5
โข ((๐ โ ฯ โง ๐ โ ฯ) โ ((๐ธโ๐) = (๐ธโ๐) โ (2o ยทo
๐) = (2o
ยทo ๐))) |
9 | | 2on 8483 |
. . . . . . 7
โข
2o โ On |
10 | 9 | a1i 11 |
. . . . . 6
โข ((๐ โ ฯ โง ๐ โ ฯ) โ
2o โ On) |
11 | | nnon 7864 |
. . . . . . 7
โข (๐ โ ฯ โ ๐ โ On) |
12 | 11 | adantr 480 |
. . . . . 6
โข ((๐ โ ฯ โง ๐ โ ฯ) โ ๐ โ On) |
13 | | nnon 7864 |
. . . . . . 7
โข (๐ โ ฯ โ ๐ โ On) |
14 | 13 | adantl 481 |
. . . . . 6
โข ((๐ โ ฯ โง ๐ โ ฯ) โ ๐ โ On) |
15 | | 0lt1o 8507 |
. . . . . . . . 9
โข โ
โ 1o |
16 | | elelsuc 6438 |
. . . . . . . . 9
โข (โ
โ 1o โ โ
โ suc 1o) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . 8
โข โ
โ suc 1o |
18 | | df-2o 8470 |
. . . . . . . 8
โข
2o = suc 1o |
19 | 17, 18 | eleqtrri 2831 |
. . . . . . 7
โข โ
โ 2o |
20 | 19 | a1i 11 |
. . . . . 6
โข ((๐ โ ฯ โง ๐ โ ฯ) โ โ
โ 2o) |
21 | | omcan 8572 |
. . . . . 6
โข
(((2o โ On โง ๐ โ On โง ๐ โ On) โง โ
โ
2o) โ ((2o ยทo ๐) = (2o ยทo ๐) โ ๐ = ๐)) |
22 | 10, 12, 14, 20, 21 | syl31anc 1372 |
. . . . 5
โข ((๐ โ ฯ โง ๐ โ ฯ) โ
((2o ยทo ๐) = (2o ยทo ๐) โ ๐ = ๐)) |
23 | 8, 22 | bitrd 278 |
. . . 4
โข ((๐ โ ฯ โง ๐ โ ฯ) โ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)) |
24 | 23 | biimpd 228 |
. . 3
โข ((๐ โ ฯ โง ๐ โ ฯ) โ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)) |
25 | 24 | rgen2 3196 |
. 2
โข
โ๐ โ
ฯ โ๐ โ
ฯ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) |
26 | | dff13 7257 |
. 2
โข (๐ธ:ฯโ1-1โฯ โ (๐ธ:ฯโถฯ โง โ๐ โ ฯ โ๐ โ ฯ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐))) |
27 | 5, 25, 26 | mpbir2an 708 |
1
โข ๐ธ:ฯโ1-1โฯ |