Step | Hyp | Ref
| Expression |
1 | | cnfcom.s |
. . . . 5
โข ๐ = dom (ฯ CNF ๐ด) |
2 | | cnfcom.a |
. . . . 5
โข (๐ โ ๐ด โ On) |
3 | | cnfcom.b |
. . . . 5
โข (๐ โ ๐ต โ (ฯ โo ๐ด)) |
4 | | cnfcom.f |
. . . . 5
โข ๐น = (โก(ฯ CNF ๐ด)โ๐ต) |
5 | | cnfcom.g |
. . . . 5
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
6 | | cnfcom.h |
. . . . 5
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)), โ
) |
7 | | cnfcom.t |
. . . . 5
โข ๐ = seqฯ((๐ โ V, ๐ โ V โฆ ๐พ), โ
) |
8 | | cnfcom.m |
. . . . 5
โข ๐ = ((ฯ โo
(๐บโ๐)) ยทo (๐นโ(๐บโ๐))) |
9 | | cnfcom.k |
. . . . 5
โข ๐พ = ((๐ฅ โ ๐ โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (๐ +o ๐ฅ))) |
10 | | ovex 7394 |
. . . . . . . . . 10
โข (๐น supp โ
) โ
V |
11 | 5 | oion 9480 |
. . . . . . . . . 10
โข ((๐น supp โ
) โ V โ
dom ๐บ โ
On) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
โข dom ๐บ โ On |
13 | 12 | elexi 3466 |
. . . . . . . 8
โข dom ๐บ โ V |
14 | 13 | uniex 7682 |
. . . . . . 7
โข โช dom ๐บ โ V |
15 | 14 | sucid 6403 |
. . . . . 6
โข โช dom ๐บ โ suc โช dom
๐บ |
16 | | cnfcom.w |
. . . . . . 7
โข ๐ = (๐บโโช dom
๐บ) |
17 | | cnfcom2.1 |
. . . . . . 7
โข (๐ โ โ
โ ๐ต) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 16,
17 | cnfcom2lem 9645 |
. . . . . 6
โข (๐ โ dom ๐บ = suc โช dom
๐บ) |
19 | 15, 18 | eleqtrrid 2841 |
. . . . 5
โข (๐ โ โช dom ๐บ โ dom ๐บ) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 19 | cnfcom 9644 |
. . . 4
โข (๐ โ (๐โsuc โช dom
๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo (๐บโโช dom ๐บ)) ยทo (๐นโ(๐บโโช dom
๐บ)))) |
21 | 16 | oveq2i 7372 |
. . . . . 6
โข (ฯ
โo ๐) =
(ฯ โo (๐บโโช dom
๐บ)) |
22 | 16 | fveq2i 6849 |
. . . . . 6
โข (๐นโ๐) = (๐นโ(๐บโโช dom
๐บ)) |
23 | 21, 22 | oveq12i 7373 |
. . . . 5
โข ((ฯ
โo ๐)
ยทo (๐นโ๐)) = ((ฯ โo (๐บโโช dom ๐บ)) ยทo (๐นโ(๐บโโช dom
๐บ))) |
24 | | f1oeq3 6778 |
. . . . 5
โข
(((ฯ โo ๐) ยทo (๐นโ๐)) = ((ฯ โo (๐บโโช dom ๐บ)) ยทo (๐นโ(๐บโโช dom
๐บ))) โ ((๐โsuc โช dom ๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)) โ (๐โsuc โช dom
๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo (๐บโโช dom ๐บ)) ยทo (๐นโ(๐บโโช dom
๐บ))))) |
25 | 23, 24 | ax-mp 5 |
. . . 4
โข ((๐โsuc โช dom ๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)) โ (๐โsuc โช dom
๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo (๐บโโช dom ๐บ)) ยทo (๐นโ(๐บโโช dom
๐บ)))) |
26 | 20, 25 | sylibr 233 |
. . 3
โข (๐ โ (๐โsuc โช dom
๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐))) |
27 | 18 | fveq2d 6850 |
. . . 4
โข (๐ โ (๐โdom ๐บ) = (๐โsuc โช dom
๐บ)) |
28 | 27 | f1oeq1d 6783 |
. . 3
โข (๐ โ ((๐โdom ๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)) โ (๐โsuc โช dom
๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)))) |
29 | 26, 28 | mpbird 257 |
. 2
โข (๐ โ (๐โdom ๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐))) |
30 | | omelon 9590 |
. . . . . . 7
โข ฯ
โ On |
31 | 30 | a1i 11 |
. . . . . 6
โข (๐ โ ฯ โ
On) |
32 | 1, 31, 2 | cantnff1o 9640 |
. . . . . . . . 9
โข (๐ โ (ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด)) |
33 | | f1ocnv 6800 |
. . . . . . . . 9
โข ((ฯ
CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐) |
34 | | f1of 6788 |
. . . . . . . . 9
โข (โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . 8
โข (๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
36 | 35, 3 | ffvelcdmd 7040 |
. . . . . . 7
โข (๐ โ (โก(ฯ CNF ๐ด)โ๐ต) โ ๐) |
37 | 4, 36 | eqeltrid 2838 |
. . . . . 6
โข (๐ โ ๐น โ ๐) |
38 | 8 | oveq1i 7371 |
. . . . . . . . . 10
โข (๐ +o ๐ง) = (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง) |
39 | 38 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ V โง ๐ง โ V) โ (๐ +o ๐ง) = (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) |
40 | 39 | mpoeq3ia 7439 |
. . . . . . . 8
โข (๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) |
41 | | eqid 2733 |
. . . . . . . 8
โข โ
=
โ
|
42 | | seqomeq12 8404 |
. . . . . . . 8
โข (((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) โง โ
= โ
) โ
seqฯ((๐
โ V, ๐ง โ V
โฆ (๐ +o
๐ง)), โ
) =
seqฯ((๐
โ V, ๐ง โ V
โฆ (((ฯ โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
)) |
43 | 40, 41, 42 | mp2an 691 |
. . . . . . 7
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
44 | 6, 43 | eqtri 2761 |
. . . . . 6
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((ฯ
โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
45 | 1, 31, 2, 5, 37, 44 | cantnfval 9612 |
. . . . 5
โข (๐ โ ((ฯ CNF ๐ด)โ๐น) = (๐ปโdom ๐บ)) |
46 | 4 | fveq2i 6849 |
. . . . 5
โข ((ฯ
CNF ๐ด)โ๐น) = ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) |
47 | 45, 46 | eqtr3di 2788 |
. . . 4
โข (๐ โ (๐ปโdom ๐บ) = ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต))) |
48 | 18 | fveq2d 6850 |
. . . 4
โข (๐ โ (๐ปโdom ๐บ) = (๐ปโsuc โช dom
๐บ)) |
49 | | f1ocnvfv2 7227 |
. . . . 5
โข
(((ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โง ๐ต โ (ฯ โo ๐ด)) โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
50 | 32, 3, 49 | syl2anc 585 |
. . . 4
โข (๐ โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
51 | 47, 48, 50 | 3eqtr3d 2781 |
. . 3
โข (๐ โ (๐ปโsuc โช dom
๐บ) = ๐ต) |
52 | 51 | f1oeq2d 6784 |
. 2
โข (๐ โ ((๐โdom ๐บ):(๐ปโsuc โช dom
๐บ)โ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)) โ (๐โdom ๐บ):๐ตโ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐)))) |
53 | 29, 52 | mpbid 231 |
1
โข (๐ โ (๐โdom ๐บ):๐ตโ1-1-ontoโ((ฯ โo ๐) ยทo (๐นโ๐))) |