Step | Hyp | Ref
| Expression |
1 | | cnfcom.w |
. . 3
โข ๐ = (๐บโโช dom
๐บ) |
2 | | cnfcom.a |
. . . 4
โข (๐ โ ๐ด โ On) |
3 | | suppssdm 8109 |
. . . . . 6
โข (๐น supp โ
) โ dom ๐น |
4 | | cnfcom.f |
. . . . . . . . 9
โข ๐น = (โก(ฯ CNF ๐ด)โ๐ต) |
5 | | cnfcom.s |
. . . . . . . . . . . 12
โข ๐ = dom (ฯ CNF ๐ด) |
6 | | omelon 9587 |
. . . . . . . . . . . . 13
โข ฯ
โ On |
7 | 6 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ ฯ โ
On) |
8 | 5, 7, 2 | cantnff1o 9637 |
. . . . . . . . . . 11
โข (๐ โ (ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด)) |
9 | | f1ocnv 6797 |
. . . . . . . . . . 11
โข ((ฯ
CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐) |
10 | | f1of 6785 |
. . . . . . . . . . 11
โข (โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
12 | | cnfcom.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ (ฯ โo ๐ด)) |
13 | 11, 12 | ffvelcdmd 7037 |
. . . . . . . . 9
โข (๐ โ (โก(ฯ CNF ๐ด)โ๐ต) โ ๐) |
14 | 4, 13 | eqeltrid 2838 |
. . . . . . . 8
โข (๐ โ ๐น โ ๐) |
15 | 5, 7, 2 | cantnfs 9607 |
. . . . . . . 8
โข (๐ โ (๐น โ ๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
))) |
16 | 14, 15 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
)) |
17 | 16 | simpld 496 |
. . . . . 6
โข (๐ โ ๐น:๐ดโถฯ) |
18 | 3, 17 | fssdm 6689 |
. . . . 5
โข (๐ โ (๐น supp โ
) โ ๐ด) |
19 | | ovex 7391 |
. . . . . . . . . . 11
โข (๐น supp โ
) โ
V |
20 | | cnfcom.g |
. . . . . . . . . . . 12
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
21 | 20 | oion 9477 |
. . . . . . . . . . 11
โข ((๐น supp โ
) โ V โ
dom ๐บ โ
On) |
22 | 19, 21 | ax-mp 5 |
. . . . . . . . . 10
โข dom ๐บ โ On |
23 | 22 | elexi 3463 |
. . . . . . . . 9
โข dom ๐บ โ V |
24 | 23 | uniex 7679 |
. . . . . . . 8
โข โช dom ๐บ โ V |
25 | 24 | sucid 6400 |
. . . . . . 7
โข โช dom ๐บ โ suc โช dom
๐บ |
26 | | cnfcom.h |
. . . . . . . 8
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)), โ
) |
27 | | cnfcom.t |
. . . . . . . 8
โข ๐ = seqฯ((๐ โ V, ๐ โ V โฆ ๐พ), โ
) |
28 | | cnfcom.m |
. . . . . . . 8
โข ๐ = ((ฯ โo
(๐บโ๐)) ยทo (๐นโ(๐บโ๐))) |
29 | | cnfcom.k |
. . . . . . . 8
โข ๐พ = ((๐ฅ โ ๐ โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (๐ +o ๐ฅ))) |
30 | | cnfcom3.1 |
. . . . . . . . 9
โข (๐ โ ฯ โ ๐ต) |
31 | | peano1 7826 |
. . . . . . . . . 10
โข โ
โ ฯ |
32 | 31 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ
โ
ฯ) |
33 | 30, 32 | sseldd 3946 |
. . . . . . . 8
โข (๐ โ โ
โ ๐ต) |
34 | 5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33 | cnfcom2lem 9642 |
. . . . . . 7
โข (๐ โ dom ๐บ = suc โช dom
๐บ) |
35 | 25, 34 | eleqtrrid 2841 |
. . . . . 6
โข (๐ โ โช dom ๐บ โ dom ๐บ) |
36 | 20 | oif 9471 |
. . . . . . 7
โข ๐บ:dom ๐บโถ(๐น supp โ
) |
37 | 36 | ffvelcdmi 7035 |
. . . . . 6
โข (โช dom ๐บ โ dom ๐บ โ (๐บโโช dom
๐บ) โ (๐น supp โ
)) |
38 | 35, 37 | syl 17 |
. . . . 5
โข (๐ โ (๐บโโช dom
๐บ) โ (๐น supp โ
)) |
39 | 18, 38 | sseldd 3946 |
. . . 4
โข (๐ โ (๐บโโช dom
๐บ) โ ๐ด) |
40 | | onelon 6343 |
. . . 4
โข ((๐ด โ On โง (๐บโโช dom ๐บ) โ ๐ด) โ (๐บโโช dom
๐บ) โ
On) |
41 | 2, 39, 40 | syl2anc 585 |
. . 3
โข (๐ โ (๐บโโช dom
๐บ) โ
On) |
42 | 1, 41 | eqeltrid 2838 |
. 2
โข (๐ โ ๐ โ On) |
43 | | oecl 8484 |
. . . . . . 7
โข ((ฯ
โ On โง ๐ด โ
On) โ (ฯ โo ๐ด) โ On) |
44 | 6, 2, 43 | sylancr 588 |
. . . . . 6
โข (๐ โ (ฯ
โo ๐ด)
โ On) |
45 | | onelon 6343 |
. . . . . 6
โข
(((ฯ โo ๐ด) โ On โง ๐ต โ (ฯ โo ๐ด)) โ ๐ต โ On) |
46 | 44, 12, 45 | syl2anc 585 |
. . . . 5
โข (๐ โ ๐ต โ On) |
47 | | ontri1 6352 |
. . . . 5
โข ((ฯ
โ On โง ๐ต โ
On) โ (ฯ โ ๐ต โ ยฌ ๐ต โ ฯ)) |
48 | 6, 46, 47 | sylancr 588 |
. . . 4
โข (๐ โ (ฯ โ ๐ต โ ยฌ ๐ต โ ฯ)) |
49 | 30, 48 | mpbid 231 |
. . 3
โข (๐ โ ยฌ ๐ต โ ฯ) |
50 | 4 | fveq2i 6846 |
. . . . . . . 8
โข ((ฯ
CNF ๐ด)โ๐น) = ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) |
51 | | f1ocnvfv2 7224 |
. . . . . . . . 9
โข
(((ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โง ๐ต โ (ฯ โo ๐ด)) โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
52 | 8, 12, 51 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((ฯ CNF ๐ด)โ(โก(ฯ CNF ๐ด)โ๐ต)) = ๐ต) |
53 | 50, 52 | eqtrid 2785 |
. . . . . . 7
โข (๐ โ ((ฯ CNF ๐ด)โ๐น) = ๐ต) |
54 | 53 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ = โ
) โ ((ฯ CNF ๐ด)โ๐น) = ๐ต) |
55 | 6 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ ฯ โ
On) |
56 | 2 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ ๐ด โ On) |
57 | 14 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ ๐น โ ๐) |
58 | 31 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ โ
โ
ฯ) |
59 | | 1on 8425 |
. . . . . . . . 9
โข
1o โ On |
60 | 59 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ 1o โ
On) |
61 | | ovexd 7393 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐น supp โ
) โ V) |
62 | 5, 7, 2, 20, 14 | cantnfcl 9608 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ( E We (๐น supp โ
) โง dom ๐บ โ ฯ)) |
63 | 62 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ E We (๐น supp โ
)) |
64 | 20 | oiiso 9478 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
65 | 61, 63, 64 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
66 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
67 | | isof1o 7269 |
. . . . . . . . . . . . . . . . . 18
โข (๐บ Isom E , E (dom ๐บ, (๐น supp โ
)) โ ๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
)) |
69 | | f1ocnv 6797 |
. . . . . . . . . . . . . . . . 17
โข (๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
) โ โก๐บ:(๐น supp โ
)โ1-1-ontoโdom
๐บ) |
70 | | f1of 6785 |
. . . . . . . . . . . . . . . . 17
โข (โก๐บ:(๐น supp โ
)โ1-1-ontoโdom
๐บ โ โก๐บ:(๐น supp โ
)โถdom ๐บ) |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ โก๐บ:(๐น supp โ
)โถdom ๐บ) |
72 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . 16
โข ((โก๐บ:(๐น supp โ
)โถdom ๐บ โง ๐ฅ โ (๐น supp โ
)) โ (โก๐บโ๐ฅ) โ dom ๐บ) |
73 | 71, 72 | sylancom 589 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โก๐บโ๐ฅ) โ dom ๐บ) |
74 | | elssuni 4899 |
. . . . . . . . . . . . . . 15
โข ((โก๐บโ๐ฅ) โ dom ๐บ โ (โก๐บโ๐ฅ) โ โช dom
๐บ) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โก๐บโ๐ฅ) โ โช dom
๐บ) |
76 | | onelon 6343 |
. . . . . . . . . . . . . . . 16
โข ((dom
๐บ โ On โง (โก๐บโ๐ฅ) โ dom ๐บ) โ (โก๐บโ๐ฅ) โ On) |
77 | 22, 73, 76 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โก๐บโ๐ฅ) โ On) |
78 | | onuni 7724 |
. . . . . . . . . . . . . . . 16
โข (dom
๐บ โ On โ โช dom ๐บ โ On) |
79 | 22, 78 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข โช dom ๐บ โ On |
80 | | ontri1 6352 |
. . . . . . . . . . . . . . 15
โข (((โก๐บโ๐ฅ) โ On โง โช dom ๐บ โ On) โ ((โก๐บโ๐ฅ) โ โช dom
๐บ โ ยฌ โช dom ๐บ โ (โก๐บโ๐ฅ))) |
81 | 77, 79, 80 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ((โก๐บโ๐ฅ) โ โช dom
๐บ โ ยฌ โช dom ๐บ โ (โก๐บโ๐ฅ))) |
82 | 75, 81 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ยฌ โช dom ๐บ โ (โก๐บโ๐ฅ)) |
83 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ โช dom ๐บ โ dom ๐บ) |
84 | | isorel 7272 |
. . . . . . . . . . . . . . . 16
โข ((๐บ Isom E , E (dom ๐บ, (๐น supp โ
)) โง (โช dom ๐บ โ dom ๐บ โง (โก๐บโ๐ฅ) โ dom ๐บ)) โ (โช dom
๐บ E (โก๐บโ๐ฅ) โ (๐บโโช dom
๐บ) E (๐บโ(โก๐บโ๐ฅ)))) |
85 | 66, 83, 73, 84 | syl12anc 836 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โช dom ๐บ E (โก๐บโ๐ฅ) โ (๐บโโช dom
๐บ) E (๐บโ(โก๐บโ๐ฅ)))) |
86 | | fvex 6856 |
. . . . . . . . . . . . . . . 16
โข (โก๐บโ๐ฅ) โ V |
87 | 86 | epeli 5540 |
. . . . . . . . . . . . . . 15
โข (โช dom ๐บ E (โก๐บโ๐ฅ) โ โช dom
๐บ โ (โก๐บโ๐ฅ)) |
88 | 1 | breq1i 5113 |
. . . . . . . . . . . . . . . 16
โข (๐ E (๐บโ(โก๐บโ๐ฅ)) โ (๐บโโช dom
๐บ) E (๐บโ(โก๐บโ๐ฅ))) |
89 | | fvex 6856 |
. . . . . . . . . . . . . . . . 17
โข (๐บโ(โก๐บโ๐ฅ)) โ V |
90 | 89 | epeli 5540 |
. . . . . . . . . . . . . . . 16
โข (๐ E (๐บโ(โก๐บโ๐ฅ)) โ ๐ โ (๐บโ(โก๐บโ๐ฅ))) |
91 | 88, 90 | bitr3i 277 |
. . . . . . . . . . . . . . 15
โข ((๐บโโช dom ๐บ) E (๐บโ(โก๐บโ๐ฅ)) โ ๐ โ (๐บโ(โก๐บโ๐ฅ))) |
92 | 85, 87, 91 | 3bitr3g 313 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โช dom ๐บ โ (โก๐บโ๐ฅ) โ ๐ โ (๐บโ(โก๐บโ๐ฅ)))) |
93 | | simplr 768 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐ = โ
) |
94 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . . . 16
โข ((๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
) โง ๐ฅ โ (๐น supp โ
)) โ (๐บโ(โก๐บโ๐ฅ)) = ๐ฅ) |
95 | 68, 94 | sylancom 589 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (๐บโ(โก๐บโ๐ฅ)) = ๐ฅ) |
96 | 93, 95 | eleq12d 2828 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (๐ โ (๐บโ(โก๐บโ๐ฅ)) โ โ
โ ๐ฅ)) |
97 | 92, 96 | bitrd 279 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (โช dom ๐บ โ (โก๐บโ๐ฅ) โ โ
โ ๐ฅ)) |
98 | 82, 97 | mtbid 324 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ยฌ โ
โ
๐ฅ) |
99 | | onss 7720 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ On โ ๐ด โ On) |
100 | 2, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ On) |
101 | 18, 100 | sstrd 3955 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐น supp โ
) โ On) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ = โ
) โ (๐น supp โ
) โ On) |
103 | 102 | sselda 3945 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐ฅ โ On) |
104 | | on0eqel 6442 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ On โ (๐ฅ = โ
โจ โ
โ
๐ฅ)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (๐ฅ = โ
โจ โ
โ ๐ฅ)) |
106 | 105 | ord 863 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ (ยฌ ๐ฅ = โ
โ โ
โ
๐ฅ)) |
107 | 98, 106 | mt3d 148 |
. . . . . . . . . . 11
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐ฅ = โ
) |
108 | | el1o 8442 |
. . . . . . . . . . 11
โข (๐ฅ โ 1o โ
๐ฅ =
โ
) |
109 | 107, 108 | sylibr 233 |
. . . . . . . . . 10
โข (((๐ โง ๐ = โ
) โง ๐ฅ โ (๐น supp โ
)) โ ๐ฅ โ 1o) |
110 | 109 | ex 414 |
. . . . . . . . 9
โข ((๐ โง ๐ = โ
) โ (๐ฅ โ (๐น supp โ
) โ ๐ฅ โ 1o)) |
111 | 110 | ssrdv 3951 |
. . . . . . . 8
โข ((๐ โง ๐ = โ
) โ (๐น supp โ
) โ
1o) |
112 | 5, 55, 56, 57, 58, 60, 111 | cantnflt2 9614 |
. . . . . . 7
โข ((๐ โง ๐ = โ
) โ ((ฯ CNF ๐ด)โ๐น) โ (ฯ โo
1o)) |
113 | | oe1 8492 |
. . . . . . . 8
โข (ฯ
โ On โ (ฯ โo 1o) =
ฯ) |
114 | 6, 113 | ax-mp 5 |
. . . . . . 7
โข (ฯ
โo 1o) = ฯ |
115 | 112, 114 | eleqtrdi 2844 |
. . . . . 6
โข ((๐ โง ๐ = โ
) โ ((ฯ CNF ๐ด)โ๐น) โ ฯ) |
116 | 54, 115 | eqeltrrd 2835 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ๐ต โ ฯ) |
117 | 116 | ex 414 |
. . . 4
โข (๐ โ (๐ = โ
โ ๐ต โ ฯ)) |
118 | 117 | necon3bd 2954 |
. . 3
โข (๐ โ (ยฌ ๐ต โ ฯ โ ๐ โ โ
)) |
119 | 49, 118 | mpd 15 |
. 2
โข (๐ โ ๐ โ โ
) |
120 | | dif1o 8447 |
. 2
โข (๐ โ (On โ
1o) โ (๐
โ On โง ๐ โ
โ
)) |
121 | 42, 119, 120 | sylanbrc 584 |
1
โข (๐ โ ๐ โ (On โ
1o)) |