Step | Hyp | Ref
| Expression |
1 | | omelon 9587 |
. . . . . 6
โข ฯ
โ On |
2 | | cnfcom.a |
. . . . . . 7
โข (๐ โ ๐ด โ On) |
3 | | suppssdm 8109 |
. . . . . . . . 9
โข (๐น supp โ
) โ dom ๐น |
4 | | cnfcom.f |
. . . . . . . . . . . 12
โข ๐น = (โก(ฯ CNF ๐ด)โ๐ต) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . 15
โข ๐ = dom (ฯ CNF ๐ด) |
6 | 1 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฯ โ
On) |
7 | 5, 6, 2 | cantnff1o 9637 |
. . . . . . . . . . . . . 14
โข (๐ โ (ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด)) |
8 | | f1ocnv 6797 |
. . . . . . . . . . . . . 14
โข ((ฯ
CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐) |
9 | | f1of 6785 |
. . . . . . . . . . . . . 14
โข (โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
11 | | cnfcom.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ (ฯ โo ๐ด)) |
12 | 10, 11 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
โข (๐ โ (โก(ฯ CNF ๐ด)โ๐ต) โ ๐) |
13 | 4, 12 | eqeltrid 2838 |
. . . . . . . . . . 11
โข (๐ โ ๐น โ ๐) |
14 | 5, 6, 2 | cantnfs 9607 |
. . . . . . . . . . 11
โข (๐ โ (๐น โ ๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
))) |
15 | 13, 14 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
)) |
16 | 15 | simpld 496 |
. . . . . . . . 9
โข (๐ โ ๐น:๐ดโถฯ) |
17 | 3, 16 | fssdm 6689 |
. . . . . . . 8
โข (๐ โ (๐น supp โ
) โ ๐ด) |
18 | | cnfcom.w |
. . . . . . . . 9
โข ๐ = (๐บโโช dom
๐บ) |
19 | | ovex 7391 |
. . . . . . . . . . . . . . 15
โข (๐น supp โ
) โ
V |
20 | | cnfcom.g |
. . . . . . . . . . . . . . . 16
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
21 | 20 | oion 9477 |
. . . . . . . . . . . . . . 15
โข ((๐น supp โ
) โ V โ
dom ๐บ โ
On) |
22 | 19, 21 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข dom ๐บ โ On |
23 | 22 | elexi 3463 |
. . . . . . . . . . . . 13
โข dom ๐บ โ V |
24 | 23 | uniex 7679 |
. . . . . . . . . . . 12
โข โช dom ๐บ โ V |
25 | 24 | sucid 6400 |
. . . . . . . . . . 11
โข โช dom ๐บ โ suc โช dom
๐บ |
26 | | cnfcom.h |
. . . . . . . . . . . 12
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)), โ
) |
27 | | cnfcom.t |
. . . . . . . . . . . 12
โข ๐ = seqฯ((๐ โ V, ๐ โ V โฆ ๐พ), โ
) |
28 | | cnfcom.m |
. . . . . . . . . . . 12
โข ๐ = ((ฯ โo
(๐บโ๐)) ยทo (๐นโ(๐บโ๐))) |
29 | | cnfcom.k |
. . . . . . . . . . . 12
โข ๐พ = ((๐ฅ โ ๐ โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (๐ +o ๐ฅ))) |
30 | | cnfcom3.1 |
. . . . . . . . . . . . 13
โข (๐ โ ฯ โ ๐ต) |
31 | | peano1 7826 |
. . . . . . . . . . . . . 14
โข โ
โ ฯ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โ
โ
ฯ) |
33 | 30, 32 | sseldd 3946 |
. . . . . . . . . . . 12
โข (๐ โ โ
โ ๐ต) |
34 | 5, 2, 11, 4, 20, 26, 27, 28, 29, 18, 33 | cnfcom2lem 9642 |
. . . . . . . . . . 11
โข (๐ โ dom ๐บ = suc โช dom
๐บ) |
35 | 25, 34 | eleqtrrid 2841 |
. . . . . . . . . 10
โข (๐ โ โช dom ๐บ โ dom ๐บ) |
36 | 20 | oif 9471 |
. . . . . . . . . . 11
โข ๐บ:dom ๐บโถ(๐น supp โ
) |
37 | 36 | ffvelcdmi 7035 |
. . . . . . . . . 10
โข (โช dom ๐บ โ dom ๐บ โ (๐บโโช dom
๐บ) โ (๐น supp โ
)) |
38 | 35, 37 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐บโโช dom
๐บ) โ (๐น supp โ
)) |
39 | 18, 38 | eqeltrid 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ (๐น supp โ
)) |
40 | 17, 39 | sseldd 3946 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ด) |
41 | | onelon 6343 |
. . . . . . 7
โข ((๐ด โ On โง ๐ โ ๐ด) โ ๐ โ On) |
42 | 2, 40, 41 | syl2anc 585 |
. . . . . 6
โข (๐ โ ๐ โ On) |
43 | | oecl 8484 |
. . . . . 6
โข ((ฯ
โ On โง ๐ โ
On) โ (ฯ โo ๐) โ On) |
44 | 1, 42, 43 | sylancr 588 |
. . . . 5
โข (๐ โ (ฯ
โo ๐)
โ On) |
45 | 16, 40 | ffvelcdmd 7037 |
. . . . . 6
โข (๐ โ (๐นโ๐) โ ฯ) |
46 | | nnon 7809 |
. . . . . 6
โข ((๐นโ๐) โ ฯ โ (๐นโ๐) โ On) |
47 | 45, 46 | syl 17 |
. . . . 5
โข (๐ โ (๐นโ๐) โ On) |
48 | | cnfcom.y |
. . . . . 6
โข ๐ = (๐ข โ (๐นโ๐), ๐ฃ โ (ฯ โo ๐) โฆ (((ฯ
โo ๐)
ยทo ๐ข)
+o ๐ฃ)) |
49 | | cnfcom.x |
. . . . . 6
โข ๐ = (๐ข โ (๐นโ๐), ๐ฃ โ (ฯ โo ๐) โฆ (((๐นโ๐) ยทo ๐ฃ) +o ๐ข)) |
50 | 48, 49 | omf1o 9022 |
. . . . 5
โข
(((ฯ โo ๐) โ On โง (๐นโ๐) โ On) โ (๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ((๐นโ๐) ยทo (ฯ
โo ๐))) |
51 | 44, 47, 50 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ((๐นโ๐) ยทo (ฯ
โo ๐))) |
52 | 16 | ffnd 6670 |
. . . . . . . . . 10
โข (๐ โ ๐น Fn ๐ด) |
53 | | 0ex 5265 |
. . . . . . . . . . 11
โข โ
โ V |
54 | 53 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ
โ
V) |
55 | | elsuppfn 8103 |
. . . . . . . . . 10
โข ((๐น Fn ๐ด โง ๐ด โ On โง โ
โ V) โ
(๐ โ (๐น supp โ
) โ (๐ โ ๐ด โง (๐นโ๐) โ โ
))) |
56 | 52, 2, 54, 55 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ โ (๐ โ (๐น supp โ
) โ (๐ โ ๐ด โง (๐นโ๐) โ โ
))) |
57 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โ ๐ด โง (๐นโ๐) โ โ
) โ (๐นโ๐) โ โ
) |
58 | 56, 57 | syl6bi 253 |
. . . . . . . 8
โข (๐ โ (๐ โ (๐น supp โ
) โ (๐นโ๐) โ โ
)) |
59 | 39, 58 | mpd 15 |
. . . . . . 7
โข (๐ โ (๐นโ๐) โ โ
) |
60 | | on0eln0 6374 |
. . . . . . . 8
โข ((๐นโ๐) โ On โ (โ
โ (๐นโ๐) โ (๐นโ๐) โ โ
)) |
61 | 45, 46, 60 | 3syl 18 |
. . . . . . 7
โข (๐ โ (โ
โ (๐นโ๐) โ (๐นโ๐) โ โ
)) |
62 | 59, 61 | mpbird 257 |
. . . . . 6
โข (๐ โ โ
โ (๐นโ๐)) |
63 | 5, 2, 11, 4, 20, 26, 27, 28, 29, 18, 30 | cnfcom3lem 9644 |
. . . . . . 7
โข (๐ โ ๐ โ (On โ
1o)) |
64 | | ondif1 8448 |
. . . . . . . 8
โข (๐ โ (On โ
1o) โ (๐
โ On โง โ
โ ๐)) |
65 | 64 | simprbi 498 |
. . . . . . 7
โข (๐ โ (On โ
1o) โ โ
โ ๐) |
66 | 63, 65 | syl 17 |
. . . . . 6
โข (๐ โ โ
โ ๐) |
67 | | omabs 8598 |
. . . . . 6
โข ((((๐นโ๐) โ ฯ โง โ
โ (๐นโ๐)) โง (๐ โ On โง โ
โ ๐)) โ ((๐นโ๐) ยทo (ฯ
โo ๐)) =
(ฯ โo ๐)) |
68 | 45, 62, 42, 66, 67 | syl22anc 838 |
. . . . 5
โข (๐ โ ((๐นโ๐) ยทo (ฯ
โo ๐)) =
(ฯ โo ๐)) |
69 | 68 | f1oeq3d 6782 |
. . . 4
โข (๐ โ ((๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ((๐นโ๐) ยทo (ฯ
โo ๐))
โ (๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ(ฯ โo ๐))) |
70 | 51, 69 | mpbid 231 |
. . 3
โข (๐ โ (๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ(ฯ โo ๐)) |
71 | 5, 2, 11, 4, 20, 26, 27, 28, 29, 18, 33 | cnfcom2 9643 |
. . 3
โข (๐ โ (๐โdom ๐บ):๐ตโ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐))) |
72 | | f1oco 6808 |
. . 3
โข (((๐ โ โก๐):((ฯ โo ๐) ยทo (๐นโ๐))โ1-1-ontoโ(ฯ โo ๐) โง (๐โdom ๐บ):๐ตโ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐))) โ ((๐ โ โก๐) โ (๐โdom ๐บ)):๐ตโ1-1-ontoโ(ฯ โo ๐)) |
73 | 70, 71, 72 | syl2anc 585 |
. 2
โข (๐ โ ((๐ โ โก๐) โ (๐โdom ๐บ)):๐ตโ1-1-ontoโ(ฯ โo ๐)) |
74 | | cnfcom.n |
. . 3
โข ๐ = ((๐ โ โก๐) โ (๐โdom ๐บ)) |
75 | | f1oeq1 6773 |
. . 3
โข (๐ = ((๐ โ โก๐) โ (๐โdom ๐บ)) โ (๐:๐ตโ1-1-ontoโ(ฯ โo ๐) โ ((๐ โ โก๐) โ (๐โdom ๐บ)):๐ตโ1-1-ontoโ(ฯ โo ๐))) |
76 | 74, 75 | ax-mp 5 |
. 2
โข (๐:๐ตโ1-1-ontoโ(ฯ โo ๐) โ ((๐ โ โก๐) โ (๐โdom ๐บ)):๐ตโ1-1-ontoโ(ฯ โo ๐)) |
77 | 73, 76 | sylibr 233 |
1
โข (๐ โ ๐:๐ตโ1-1-ontoโ(ฯ โo ๐)) |