Step | Hyp | Ref
| Expression |
1 | | infxpenc.6 |
. . . 4
โข (๐ โ ๐:๐ดโ1-1-ontoโ(ฯ โo ๐)) |
2 | | f1ocnv 6797 |
. . . 4
โข (๐:๐ดโ1-1-ontoโ(ฯ โo ๐) โ โก๐:(ฯ โo ๐)โ1-1-ontoโ๐ด) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ โ โก๐:(ฯ โo ๐)โ1-1-ontoโ๐ด) |
4 | | infxpenc.4 |
. . . . . . . 8
โข (๐ โ ๐น:(ฯ โo
2o)โ1-1-ontoโฯ) |
5 | | f1oi 6823 |
. . . . . . . . 9
โข ( I
โพ ๐):๐โ1-1-ontoโ๐ |
6 | 5 | a1i 11 |
. . . . . . . 8
โข (๐ โ ( I โพ ๐):๐โ1-1-ontoโ๐) |
7 | | omelon 9587 |
. . . . . . . . . . 11
โข ฯ
โ On |
8 | 7 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ ฯ โ
On) |
9 | | 2on 8427 |
. . . . . . . . . 10
โข
2o โ On |
10 | | oecl 8484 |
. . . . . . . . . 10
โข ((ฯ
โ On โง 2o โ On) โ (ฯ โo
2o) โ On) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (ฯ
โo 2o) โ On) |
12 | 9 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2o โ
On) |
13 | | peano1 7826 |
. . . . . . . . . . 11
โข โ
โ ฯ |
14 | 13 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ
โ
ฯ) |
15 | | oen0 8534 |
. . . . . . . . . 10
โข
(((ฯ โ On โง 2o โ On) โง โ
โ
ฯ) โ โ
โ (ฯ โo
2o)) |
16 | 8, 12, 14, 15 | syl21anc 837 |
. . . . . . . . 9
โข (๐ โ โ
โ (ฯ
โo 2o)) |
17 | | ondif1 8448 |
. . . . . . . . 9
โข ((ฯ
โo 2o) โ (On โ 1o) โ
((ฯ โo 2o) โ On โง โ
โ
(ฯ โo 2o))) |
18 | 11, 16, 17 | sylanbrc 584 |
. . . . . . . 8
โข (๐ โ (ฯ
โo 2o) โ (On โ
1o)) |
19 | | infxpenc.3 |
. . . . . . . . 9
โข (๐ โ ๐ โ (On โ
1o)) |
20 | 19 | eldifad 3923 |
. . . . . . . 8
โข (๐ โ ๐ โ On) |
21 | | infxpenc.5 |
. . . . . . . 8
โข (๐ โ (๐นโโ
) = โ
) |
22 | | infxpenc.k |
. . . . . . . 8
โข ๐พ = (๐ฆ โ {๐ฅ โ ((ฯ โo
2o) โm ๐) โฃ ๐ฅ finSupp โ
} โฆ (๐น โ (๐ฆ โ โก( I โพ ๐)))) |
23 | | infxpenc.h |
. . . . . . . 8
โข ๐ป = (((ฯ CNF ๐) โ ๐พ) โ โก((ฯ โo 2o)
CNF ๐)) |
24 | 4, 6, 18, 20, 8, 20, 21, 22, 23 | oef1o 9639 |
. . . . . . 7
โข (๐ โ ๐ป:((ฯ โo 2o)
โo ๐)โ1-1-ontoโ(ฯ โo ๐)) |
25 | | f1oi 6823 |
. . . . . . . . . 10
โข ( I
โพ ฯ):ฯโ1-1-ontoโฯ |
26 | 25 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ( I โพ
ฯ):ฯโ1-1-ontoโฯ) |
27 | | infxpenc.x |
. . . . . . . . . . 11
โข ๐ = (๐ง โ 2o, ๐ค โ ๐ โฆ ((๐ ยทo ๐ง) +o ๐ค)) |
28 | | infxpenc.y |
. . . . . . . . . . 11
โข ๐ = (๐ง โ 2o, ๐ค โ ๐ โฆ ((2o
ยทo ๐ค)
+o ๐ง)) |
29 | 27, 28 | omf1o 9022 |
. . . . . . . . . 10
โข ((๐ โ On โง 2o
โ On) โ (๐
โ โก๐):(๐ ยทo
2o)โ1-1-ontoโ(2o ยทo ๐)) |
30 | 20, 9, 29 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (๐ โ โก๐):(๐ ยทo
2o)โ1-1-ontoโ(2o ยทo ๐)) |
31 | | ondif1 8448 |
. . . . . . . . . . 11
โข (ฯ
โ (On โ 1o) โ (ฯ โ On โง โ
โ ฯ)) |
32 | 7, 13, 31 | mpbir2an 710 |
. . . . . . . . . 10
โข ฯ
โ (On โ 1o) |
33 | 32 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ฯ โ (On โ
1o)) |
34 | | omcl 8483 |
. . . . . . . . . 10
โข ((๐ โ On โง 2o
โ On) โ (๐
ยทo 2o) โ On) |
35 | 20, 9, 34 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (๐ ยทo 2o) โ
On) |
36 | | omcl 8483 |
. . . . . . . . . 10
โข
((2o โ On โง ๐ โ On) โ (2o
ยทo ๐)
โ On) |
37 | 12, 20, 36 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (2o
ยทo ๐)
โ On) |
38 | | fvresi 7120 |
. . . . . . . . . 10
โข (โ
โ ฯ โ (( I โพ ฯ)โโ
) =
โ
) |
39 | 13, 38 | mp1i 13 |
. . . . . . . . 9
โข (๐ โ (( I โพ
ฯ)โโ
) = โ
) |
40 | | infxpenc.l |
. . . . . . . . 9
โข ๐ฟ = (๐ฆ โ {๐ฅ โ (ฯ โm (๐ ยทo
2o)) โฃ ๐ฅ
finSupp โ
} โฆ (( I โพ ฯ) โ (๐ฆ โ โก(๐ โ โก๐)))) |
41 | | infxpenc.j |
. . . . . . . . 9
โข ๐ฝ = (((ฯ CNF (2o
ยทo ๐))
โ ๐ฟ) โ โก(ฯ CNF (๐ ยทo
2o))) |
42 | 26, 30, 33, 35, 8, 37, 39, 40, 41 | oef1o 9639 |
. . . . . . . 8
โข (๐ โ ๐ฝ:(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ(ฯ โo (2o
ยทo ๐))) |
43 | | oeoe 8547 |
. . . . . . . . . 10
โข ((ฯ
โ On โง 2o โ On โง ๐ โ On) โ ((ฯ
โo 2o) โo ๐) = (ฯ โo
(2o ยทo ๐))) |
44 | 7, 12, 20, 43 | mp3an2i 1467 |
. . . . . . . . 9
โข (๐ โ ((ฯ
โo 2o) โo ๐) = (ฯ โo
(2o ยทo ๐))) |
45 | 44 | f1oeq3d 6782 |
. . . . . . . 8
โข (๐ โ (๐ฝ:(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ((ฯ โo 2o)
โo ๐)
โ ๐ฝ:(ฯ
โo (๐
ยทo 2o))โ1-1-ontoโ(ฯ โo (2o
ยทo ๐)))) |
46 | 42, 45 | mpbird 257 |
. . . . . . 7
โข (๐ โ ๐ฝ:(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ((ฯ โo 2o)
โo ๐)) |
47 | | f1oco 6808 |
. . . . . . 7
โข ((๐ป:((ฯ โo
2o) โo ๐)โ1-1-ontoโ(ฯ โo ๐) โง ๐ฝ:(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ((ฯ โo 2o)
โo ๐))
โ (๐ป โ ๐ฝ):(ฯ โo
(๐ ยทo
2o))โ1-1-ontoโ(ฯ โo ๐)) |
48 | 24, 46, 47 | syl2anc 585 |
. . . . . 6
โข (๐ โ (๐ป โ ๐ฝ):(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ(ฯ โo ๐)) |
49 | | df-2o 8414 |
. . . . . . . . . . . 12
โข
2o = suc 1o |
50 | 49 | oveq2i 7369 |
. . . . . . . . . . 11
โข (๐ ยทo
2o) = (๐
ยทo suc 1o) |
51 | | 1on 8425 |
. . . . . . . . . . . 12
โข
1o โ On |
52 | | omsuc 8473 |
. . . . . . . . . . . 12
โข ((๐ โ On โง 1o
โ On) โ (๐
ยทo suc 1o) = ((๐ ยทo 1o)
+o ๐)) |
53 | 20, 51, 52 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยทo suc 1o) =
((๐ ยทo
1o) +o ๐)) |
54 | 50, 53 | eqtrid 2785 |
. . . . . . . . . 10
โข (๐ โ (๐ ยทo 2o) =
((๐ ยทo
1o) +o ๐)) |
55 | | om1 8490 |
. . . . . . . . . . . 12
โข (๐ โ On โ (๐ ยทo
1o) = ๐) |
56 | 20, 55 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยทo 1o) = ๐) |
57 | 56 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยทo 1o)
+o ๐) = (๐ +o ๐)) |
58 | 54, 57 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ (๐ ยทo 2o) =
(๐ +o ๐)) |
59 | 58 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (ฯ
โo (๐
ยทo 2o)) = (ฯ โo (๐ +o ๐))) |
60 | | oeoa 8545 |
. . . . . . . . 9
โข ((ฯ
โ On โง ๐ โ On
โง ๐ โ On) โ
(ฯ โo (๐ +o ๐)) = ((ฯ โo ๐) ยทo (ฯ
โo ๐))) |
61 | 7, 20, 20, 60 | mp3an2i 1467 |
. . . . . . . 8
โข (๐ โ (ฯ
โo (๐
+o ๐)) =
((ฯ โo ๐) ยทo (ฯ
โo ๐))) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ (ฯ
โo (๐
ยทo 2o)) = ((ฯ โo ๐) ยทo (ฯ
โo ๐))) |
63 | 62 | f1oeq2d 6781 |
. . . . . 6
โข (๐ โ ((๐ป โ ๐ฝ):(ฯ โo (๐ ยทo
2o))โ1-1-ontoโ(ฯ โo ๐) โ (๐ป โ ๐ฝ):((ฯ โo ๐) ยทo (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐))) |
64 | 48, 63 | mpbid 231 |
. . . . 5
โข (๐ โ (๐ป โ ๐ฝ):((ฯ โo ๐) ยทo (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐)) |
65 | | oecl 8484 |
. . . . . . 7
โข ((ฯ
โ On โง ๐ โ
On) โ (ฯ โo ๐) โ On) |
66 | 8, 20, 65 | syl2anc 585 |
. . . . . 6
โข (๐ โ (ฯ
โo ๐)
โ On) |
67 | | infxpenc.z |
. . . . . . 7
โข ๐ = (๐ฅ โ (ฯ โo ๐), ๐ฆ โ (ฯ โo ๐) โฆ (((ฯ
โo ๐)
ยทo ๐ฅ)
+o ๐ฆ)) |
68 | 67 | omxpenlem 9020 |
. . . . . 6
โข
(((ฯ โo ๐) โ On โง (ฯ
โo ๐)
โ On) โ ๐:((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ((ฯ โo ๐) ยทo (ฯ
โo ๐))) |
69 | 66, 66, 68 | syl2anc 585 |
. . . . 5
โข (๐ โ ๐:((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ((ฯ โo ๐) ยทo (ฯ
โo ๐))) |
70 | | f1oco 6808 |
. . . . 5
โข (((๐ป โ ๐ฝ):((ฯ โo ๐) ยทo (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐) โง ๐:((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ((ฯ โo ๐) ยทo (ฯ
โo ๐)))
โ ((๐ป โ ๐ฝ) โ ๐):((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐)) |
71 | 64, 69, 70 | syl2anc 585 |
. . . 4
โข (๐ โ ((๐ป โ ๐ฝ) โ ๐):((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐)) |
72 | | f1of 6785 |
. . . . . . . . . 10
โข (๐:๐ดโ1-1-ontoโ(ฯ โo ๐) โ ๐:๐ดโถ(ฯ โo ๐)) |
73 | 1, 72 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐:๐ดโถ(ฯ โo ๐)) |
74 | 73 | feqmptd 6911 |
. . . . . . . 8
โข (๐ โ ๐ = (๐ฅ โ ๐ด โฆ (๐โ๐ฅ))) |
75 | 74 | f1oeq1d 6780 |
. . . . . . 7
โข (๐ โ (๐:๐ดโ1-1-ontoโ(ฯ โo ๐) โ (๐ฅ โ ๐ด โฆ (๐โ๐ฅ)):๐ดโ1-1-ontoโ(ฯ โo ๐))) |
76 | 1, 75 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐โ๐ฅ)):๐ดโ1-1-ontoโ(ฯ โo ๐)) |
77 | 73 | feqmptd 6911 |
. . . . . . . 8
โข (๐ โ ๐ = (๐ฆ โ ๐ด โฆ (๐โ๐ฆ))) |
78 | 77 | f1oeq1d 6780 |
. . . . . . 7
โข (๐ โ (๐:๐ดโ1-1-ontoโ(ฯ โo ๐) โ (๐ฆ โ ๐ด โฆ (๐โ๐ฆ)):๐ดโ1-1-ontoโ(ฯ โo ๐))) |
79 | 1, 78 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ฆ โ ๐ด โฆ (๐โ๐ฆ)):๐ดโ1-1-ontoโ(ฯ โo ๐)) |
80 | 76, 79 | xpf1o 9086 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ด โฆ โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ):(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐))) |
81 | | infxpenc.t |
. . . . . 6
โข ๐ = (๐ฅ โ ๐ด, ๐ฆ โ ๐ด โฆ โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ) |
82 | | f1oeq1 6773 |
. . . . . 6
โข (๐ = (๐ฅ โ ๐ด, ๐ฆ โ ๐ด โฆ โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ) โ (๐:(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐)) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ด โฆ โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ):(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐)))) |
83 | 81, 82 | ax-mp 5 |
. . . . 5
โข (๐:(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐)) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ด โฆ โจ(๐โ๐ฅ), (๐โ๐ฆ)โฉ):(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐))) |
84 | 80, 83 | sylibr 233 |
. . . 4
โข (๐ โ ๐:(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐))) |
85 | | f1oco 6808 |
. . . 4
โข ((((๐ป โ ๐ฝ) โ ๐):((ฯ โo ๐) ร (ฯ
โo ๐))โ1-1-ontoโ(ฯ โo ๐) โง ๐:(๐ด ร ๐ด)โ1-1-ontoโ((ฯ โo ๐) ร (ฯ โo ๐))) โ (((๐ป โ ๐ฝ) โ ๐) โ ๐):(๐ด ร ๐ด)โ1-1-ontoโ(ฯ โo ๐)) |
86 | 71, 84, 85 | syl2anc 585 |
. . 3
โข (๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐):(๐ด ร ๐ด)โ1-1-ontoโ(ฯ โo ๐)) |
87 | | f1oco 6808 |
. . 3
โข ((โก๐:(ฯ โo ๐)โ1-1-ontoโ๐ด โง (((๐ป โ ๐ฝ) โ ๐) โ ๐):(๐ด ร ๐ด)โ1-1-ontoโ(ฯ โo ๐)) โ (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)):(๐ด ร ๐ด)โ1-1-ontoโ๐ด) |
88 | 3, 86, 87 | syl2anc 585 |
. 2
โข (๐ โ (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)):(๐ด ร ๐ด)โ1-1-ontoโ๐ด) |
89 | | infxpenc.g |
. . 3
โข ๐บ = (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)) |
90 | | f1oeq1 6773 |
. . 3
โข (๐บ = (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)) โ (๐บ:(๐ด ร ๐ด)โ1-1-ontoโ๐ด โ (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)):(๐ด ร ๐ด)โ1-1-ontoโ๐ด)) |
91 | 89, 90 | ax-mp 5 |
. 2
โข (๐บ:(๐ด ร ๐ด)โ1-1-ontoโ๐ด โ (โก๐ โ (((๐ป โ ๐ฝ) โ ๐) โ ๐)):(๐ด ร ๐ด)โ1-1-ontoโ๐ด) |
92 | 88, 91 | sylibr 233 |
1
โข (๐ โ ๐บ:(๐ด ร ๐ด)โ1-1-ontoโ๐ด) |