Step | Hyp | Ref
| Expression |
1 | | cnfcom2.1 |
. . . . . 6
โข (๐ โ โ
โ ๐ต) |
2 | | n0i 4297 |
. . . . . 6
โข (โ
โ ๐ต โ ยฌ ๐ต = โ
) |
3 | 1, 2 | syl 17 |
. . . . 5
โข (๐ โ ยฌ ๐ต = โ
) |
4 | | cnfcom.f |
. . . . . . . . . . . . . 14
โข ๐น = (โก(ฯ CNF ๐ด)โ๐ต) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . . 17
โข ๐ = dom (ฯ CNF ๐ด) |
6 | | omelon 9590 |
. . . . . . . . . . . . . . . . . 18
โข ฯ
โ On |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ฯ โ
On) |
8 | | cnfcom.a |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ On) |
9 | 5, 7, 8 | cantnff1o 9640 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด)) |
10 | | f1ocnv 6800 |
. . . . . . . . . . . . . . . 16
โข ((ฯ
CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐) |
11 | | f1of 6788 |
. . . . . . . . . . . . . . . 16
โข (โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . 15
โข (๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
13 | | cnfcom.b |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ (ฯ โo ๐ด)) |
14 | 12, 13 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
โข (๐ โ (โก(ฯ CNF ๐ด)โ๐ต) โ ๐) |
15 | 4, 14 | eqeltrid 2838 |
. . . . . . . . . . . . 13
โข (๐ โ ๐น โ ๐) |
16 | 5, 7, 8 | cantnfs 9610 |
. . . . . . . . . . . . 13
โข (๐ โ (๐น โ ๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
))) |
17 | 15, 16 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
)) |
18 | 17 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐น:๐ดโถฯ) |
19 | 18 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง dom ๐บ = โ
) โ ๐น:๐ดโถฯ) |
20 | 19 | feqmptd 6914 |
. . . . . . . . 9
โข ((๐ โง dom ๐บ = โ
) โ ๐น = (๐ฅ โ ๐ด โฆ (๐นโ๐ฅ))) |
21 | | dif0 4336 |
. . . . . . . . . . . 12
โข (๐ด โ โ
) = ๐ด |
22 | 21 | eleq2i 2826 |
. . . . . . . . . . 11
โข (๐ฅ โ (๐ด โ โ
) โ ๐ฅ โ ๐ด) |
23 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง dom ๐บ = โ
) โ dom ๐บ = โ
) |
24 | | ovexd 7396 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐น supp โ
) โ V) |
25 | | cnfcom.g |
. . . . . . . . . . . . . . . . . . . 20
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
26 | 5, 7, 8, 25, 15 | cantnfcl 9611 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ( E We (๐น supp โ
) โง dom ๐บ โ ฯ)) |
27 | 26 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ E We (๐น supp โ
)) |
28 | 25 | oien 9482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
dom ๐บ โ (๐น supp โ
)) |
29 | 24, 27, 28 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ dom ๐บ โ (๐น supp โ
)) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง dom ๐บ = โ
) โ dom ๐บ โ (๐น supp โ
)) |
31 | 23, 30 | eqbrtrrd 5133 |
. . . . . . . . . . . . . . 15
โข ((๐ โง dom ๐บ = โ
) โ โ
โ (๐น supp โ
)) |
32 | 31 | ensymd 8951 |
. . . . . . . . . . . . . 14
โข ((๐ โง dom ๐บ = โ
) โ (๐น supp โ
) โ
โ
) |
33 | | en0 8963 |
. . . . . . . . . . . . . 14
โข ((๐น supp โ
) โ โ
โ (๐น supp โ
) =
โ
) |
34 | 32, 33 | sylib 217 |
. . . . . . . . . . . . 13
โข ((๐ โง dom ๐บ = โ
) โ (๐น supp โ
) = โ
) |
35 | | ss0b 4361 |
. . . . . . . . . . . . 13
โข ((๐น supp โ
) โ โ
โ (๐น supp โ
) =
โ
) |
36 | 34, 35 | sylibr 233 |
. . . . . . . . . . . 12
โข ((๐ โง dom ๐บ = โ
) โ (๐น supp โ
) โ
โ
) |
37 | 8 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง dom ๐บ = โ
) โ ๐ด โ On) |
38 | | 0ex 5268 |
. . . . . . . . . . . . 13
โข โ
โ V |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง dom ๐บ = โ
) โ โ
โ
V) |
40 | 19, 36, 37, 39 | suppssr 8131 |
. . . . . . . . . . 11
โข (((๐ โง dom ๐บ = โ
) โง ๐ฅ โ (๐ด โ โ
)) โ (๐นโ๐ฅ) = โ
) |
41 | 22, 40 | sylan2br 596 |
. . . . . . . . . 10
โข (((๐ โง dom ๐บ = โ
) โง ๐ฅ โ ๐ด) โ (๐นโ๐ฅ) = โ
) |
42 | 41 | mpteq2dva 5209 |
. . . . . . . . 9
โข ((๐ โง dom ๐บ = โ
) โ (๐ฅ โ ๐ด โฆ (๐นโ๐ฅ)) = (๐ฅ โ ๐ด โฆ โ
)) |
43 | 20, 42 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ โง dom ๐บ = โ
) โ ๐น = (๐ฅ โ ๐ด โฆ โ
)) |
44 | | fconstmpt 5698 |
. . . . . . . 8
โข (๐ด ร {โ
}) = (๐ฅ โ ๐ด โฆ โ
) |
45 | 43, 44 | eqtr4di 2791 |
. . . . . . 7
โข ((๐ โง dom ๐บ = โ
) โ ๐น = (๐ด ร {โ
})) |
46 | 45 | fveq2d 6850 |
. . . . . 6
โข ((๐ โง dom ๐บ = โ
) โ ((ฯ CNF ๐ด)โ๐น) = ((ฯ CNF ๐ด)โ(๐ด ร {โ
}))) |
47 | 4 | fveq2i 6849 |
. . . . . . . 8
โข ((ฯ
CNF ๐ด)โ๐น) = ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) |
48 | | f1ocnvfv2 7227 |
. . . . . . . . 9
โข
(((ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โง ๐ต โ (ฯ โo ๐ด)) โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
49 | 9, 13, 48 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
50 | 47, 49 | eqtrid 2785 |
. . . . . . 7
โข (๐ โ ((ฯ CNF ๐ด)โ๐น) = ๐ต) |
51 | 50 | adantr 482 |
. . . . . 6
โข ((๐ โง dom ๐บ = โ
) โ ((ฯ CNF ๐ด)โ๐น) = ๐ต) |
52 | | peano1 7829 |
. . . . . . . . 9
โข โ
โ ฯ |
53 | 52 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ
โ
ฯ) |
54 | 5, 7, 8, 53 | cantnf0 9619 |
. . . . . . 7
โข (๐ โ ((ฯ CNF ๐ด)โ(๐ด ร {โ
})) =
โ
) |
55 | 54 | adantr 482 |
. . . . . 6
โข ((๐ โง dom ๐บ = โ
) โ ((ฯ CNF ๐ด)โ(๐ด ร {โ
})) =
โ
) |
56 | 46, 51, 55 | 3eqtr3d 2781 |
. . . . 5
โข ((๐ โง dom ๐บ = โ
) โ ๐ต = โ
) |
57 | 3, 56 | mtand 815 |
. . . 4
โข (๐ โ ยฌ dom ๐บ = โ
) |
58 | | nnlim 7820 |
. . . . 5
โข (dom
๐บ โ ฯ โ
ยฌ Lim dom ๐บ) |
59 | 26, 58 | simpl2im 505 |
. . . 4
โข (๐ โ ยฌ Lim dom ๐บ) |
60 | | ioran 983 |
. . . 4
โข (ยฌ
(dom ๐บ = โ
โจ Lim
dom ๐บ) โ (ยฌ dom
๐บ = โ
โง ยฌ Lim
dom ๐บ)) |
61 | 57, 59, 60 | sylanbrc 584 |
. . 3
โข (๐ โ ยฌ (dom ๐บ = โ
โจ Lim dom ๐บ)) |
62 | 25 | oicl 9473 |
. . . 4
โข Ord dom
๐บ |
63 | | unizlim 6444 |
. . . 4
โข (Ord dom
๐บ โ (dom ๐บ = โช
dom ๐บ โ (dom ๐บ = โ
โจ Lim dom ๐บ))) |
64 | 62, 63 | ax-mp 5 |
. . 3
โข (dom
๐บ = โช dom ๐บ โ (dom ๐บ = โ
โจ Lim dom ๐บ)) |
65 | 61, 64 | sylnibr 329 |
. 2
โข (๐ โ ยฌ dom ๐บ = โช
dom ๐บ) |
66 | | orduniorsuc 7769 |
. . . 4
โข (Ord dom
๐บ โ (dom ๐บ = โช
dom ๐บ โจ dom ๐บ = suc โช dom ๐บ)) |
67 | 62, 66 | mp1i 13 |
. . 3
โข (๐ โ (dom ๐บ = โช dom ๐บ โจ dom ๐บ = suc โช dom
๐บ)) |
68 | 67 | ord 863 |
. 2
โข (๐ โ (ยฌ dom ๐บ = โช
dom ๐บ โ dom ๐บ = suc โช dom ๐บ)) |
69 | 65, 68 | mpd 15 |
1
โข (๐ โ dom ๐บ = suc โช dom
๐บ) |