Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
โข ๐ = dom (๐ด CNF ๐ต) |
2 | | cantnfs.a |
. . 3
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . 3
โข (๐ โ ๐ต โ On) |
4 | | cantnfp1.o |
. . 3
โข ๐ = OrdIso( E , (๐น supp โ
)) |
5 | | cantnfp1.g |
. . . 4
โข (๐ โ ๐บ โ ๐) |
6 | | cantnfp1.x |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
7 | | cantnfp1.y |
. . . 4
โข (๐ โ ๐ โ ๐ด) |
8 | | cantnfp1.s |
. . . 4
โข (๐ โ (๐บ supp โ
) โ ๐) |
9 | | cantnfp1.f |
. . . 4
โข ๐น = (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) |
10 | 1, 2, 3, 5, 6, 7, 8, 9 | cantnfp1lem1 9619 |
. . 3
โข (๐ โ ๐น โ ๐) |
11 | | cantnfp1.h |
. . 3
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐โ๐)) ยทo (๐นโ(๐โ๐))) +o ๐ง)), โ
) |
12 | 1, 2, 3, 4, 10, 11 | cantnfval 9609 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (๐ปโdom ๐)) |
13 | | cantnfp1.e |
. . . 4
โข (๐ โ โ
โ ๐) |
14 | 1, 2, 3, 5, 6, 7, 8, 9, 13, 4 | cantnfp1lem2 9620 |
. . 3
โข (๐ โ dom ๐ = suc โช dom
๐) |
15 | 14 | fveq2d 6847 |
. 2
โข (๐ โ (๐ปโdom ๐) = (๐ปโsuc โช dom
๐)) |
16 | 1, 2, 3, 4, 10 | cantnfcl 9608 |
. . . . . . 7
โข (๐ โ ( E We (๐น supp โ
) โง dom ๐ โ ฯ)) |
17 | 16 | simprd 497 |
. . . . . 6
โข (๐ โ dom ๐ โ ฯ) |
18 | 14, 17 | eqeltrrd 2835 |
. . . . 5
โข (๐ โ suc โช dom ๐ โ ฯ) |
19 | | peano2b 7820 |
. . . . 5
โข (โช dom ๐ โ ฯ โ suc โช dom ๐ โ ฯ) |
20 | 18, 19 | sylibr 233 |
. . . 4
โข (๐ โ โช dom ๐ โ ฯ) |
21 | 1, 2, 3, 4, 10, 11 | cantnfsuc 9611 |
. . . 4
โข ((๐ โง โช dom ๐ โ ฯ) โ (๐ปโsuc โช dom
๐) = (((๐ด โo (๐โโช dom
๐)) ยทo
(๐นโ(๐โโช dom
๐))) +o (๐ปโโช dom ๐))) |
22 | 20, 21 | mpdan 686 |
. . 3
โข (๐ โ (๐ปโsuc โช dom
๐) = (((๐ด โo (๐โโช dom
๐)) ยทo
(๐นโ(๐โโช dom
๐))) +o (๐ปโโช dom ๐))) |
23 | | ovexd 7393 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐น supp โ
) โ V) |
24 | 16 | simpld 496 |
. . . . . . . . . . . . . . 15
โข (๐ โ E We (๐น supp โ
)) |
25 | 4 | oiiso 9478 |
. . . . . . . . . . . . . . 15
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
๐ Isom E , E (dom ๐, (๐น supp โ
))) |
26 | 23, 24, 25 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ Isom E , E (dom ๐, (๐น supp โ
))) |
27 | | isof1o 7269 |
. . . . . . . . . . . . . 14
โข (๐ Isom E , E (dom ๐, (๐น supp โ
)) โ ๐:dom ๐โ1-1-ontoโ(๐น supp โ
)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐:dom ๐โ1-1-ontoโ(๐น supp โ
)) |
29 | | f1ocnv 6797 |
. . . . . . . . . . . . 13
โข (๐:dom ๐โ1-1-ontoโ(๐น supp โ
) โ โก๐:(๐น supp โ
)โ1-1-ontoโdom
๐) |
30 | | f1of 6785 |
. . . . . . . . . . . . 13
โข (โก๐:(๐น supp โ
)โ1-1-ontoโdom
๐ โ โก๐:(๐น supp โ
)โถdom ๐) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ โก๐:(๐น supp โ
)โถdom ๐) |
32 | | iftrue 4493 |
. . . . . . . . . . . . . . 15
โข (๐ก = ๐ โ if(๐ก = ๐, ๐, (๐บโ๐ก)) = ๐) |
33 | 9, 32, 6, 7 | fvmptd3 6972 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐นโ๐) = ๐) |
34 | 13 | ne0d 4296 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ
) |
35 | 33, 34 | eqnetrd 3008 |
. . . . . . . . . . . . 13
โข (๐ โ (๐นโ๐) โ โ
) |
36 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ ๐ต) โ ๐ โ ๐ด) |
37 | 1, 2, 3 | cantnfs 9607 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ โ ๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
))) |
38 | 5, 37 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
)) |
39 | 38 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บ:๐ตโถ๐ด) |
40 | 39 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ ๐ต) โ (๐บโ๐ก) โ ๐ด) |
41 | 36, 40 | ifcld 4533 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ก โ ๐ต) โ if(๐ก = ๐, ๐, (๐บโ๐ก)) โ ๐ด) |
42 | 41, 9 | fmptd 7063 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐น:๐ตโถ๐ด) |
43 | 42 | ffnd 6670 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐น Fn ๐ต) |
44 | | 0ex 5265 |
. . . . . . . . . . . . . . 15
โข โ
โ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ
โ
V) |
46 | | elsuppfn 8103 |
. . . . . . . . . . . . . 14
โข ((๐น Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ โ (๐น supp โ
) โ (๐ โ ๐ต โง (๐นโ๐) โ โ
))) |
47 | 43, 3, 45, 46 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (๐น supp โ
) โ (๐ โ ๐ต โง (๐นโ๐) โ โ
))) |
48 | 6, 35, 47 | mpbir2and 712 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐น supp โ
)) |
49 | 31, 48 | ffvelcdmd 7037 |
. . . . . . . . . . 11
โข (๐ โ (โก๐โ๐) โ dom ๐) |
50 | | elssuni 4899 |
. . . . . . . . . . 11
โข ((โก๐โ๐) โ dom ๐ โ (โก๐โ๐) โ โช dom
๐) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โก๐โ๐) โ โช dom
๐) |
52 | 4 | oicl 9470 |
. . . . . . . . . . . 12
โข Ord dom
๐ |
53 | | ordelon 6342 |
. . . . . . . . . . . 12
โข ((Ord dom
๐ โง (โก๐โ๐) โ dom ๐) โ (โก๐โ๐) โ On) |
54 | 52, 49, 53 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (โก๐โ๐) โ On) |
55 | | nnon 7809 |
. . . . . . . . . . . 12
โข (โช dom ๐ โ ฯ โ โช dom ๐ โ On) |
56 | 20, 55 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โช dom ๐ โ On) |
57 | | ontri1 6352 |
. . . . . . . . . . 11
โข (((โก๐โ๐) โ On โง โช dom ๐ โ On) โ ((โก๐โ๐) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐))) |
58 | 54, 56, 57 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((โก๐โ๐) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐))) |
59 | 51, 58 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ ยฌ โช dom ๐ โ (โก๐โ๐)) |
60 | | sucidg 6399 |
. . . . . . . . . . . . . 14
โข (โช dom ๐ โ ฯ โ โช dom ๐ โ suc โช dom
๐) |
61 | 20, 60 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โช dom ๐ โ suc โช dom
๐) |
62 | 61, 14 | eleqtrrd 2837 |
. . . . . . . . . . . 12
โข (๐ โ โช dom ๐ โ dom ๐) |
63 | | isorel 7272 |
. . . . . . . . . . . 12
โข ((๐ Isom E , E (dom ๐, (๐น supp โ
)) โง (โช dom ๐ โ dom ๐ โง (โก๐โ๐) โ dom ๐)) โ (โช dom
๐ E (โก๐โ๐) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐)))) |
64 | 26, 62, 49, 63 | syl12anc 836 |
. . . . . . . . . . 11
โข (๐ โ (โช dom ๐ E (โก๐โ๐) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐)))) |
65 | | fvex 6856 |
. . . . . . . . . . . 12
โข (โก๐โ๐) โ V |
66 | 65 | epeli 5540 |
. . . . . . . . . . 11
โข (โช dom ๐ E (โก๐โ๐) โ โช dom
๐ โ (โก๐โ๐)) |
67 | | fvex 6856 |
. . . . . . . . . . . 12
โข (๐โ(โก๐โ๐)) โ V |
68 | 67 | epeli 5540 |
. . . . . . . . . . 11
โข ((๐โโช dom ๐) E (๐โ(โก๐โ๐)) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐))) |
69 | 64, 66, 68 | 3bitr3g 313 |
. . . . . . . . . 10
โข (๐ โ (โช dom ๐ โ (โก๐โ๐) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐)))) |
70 | | f1ocnvfv2 7224 |
. . . . . . . . . . . 12
โข ((๐:dom ๐โ1-1-ontoโ(๐น supp โ
) โง ๐ โ (๐น supp โ
)) โ (๐โ(โก๐โ๐)) = ๐) |
71 | 28, 48, 70 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐โ(โก๐โ๐)) = ๐) |
72 | 71 | eleq2d 2820 |
. . . . . . . . . 10
โข (๐ โ ((๐โโช dom
๐) โ (๐โ(โก๐โ๐)) โ (๐โโช dom
๐) โ ๐)) |
73 | 69, 72 | bitrd 279 |
. . . . . . . . 9
โข (๐ โ (โช dom ๐ โ (โก๐โ๐) โ (๐โโช dom
๐) โ ๐)) |
74 | 59, 73 | mtbid 324 |
. . . . . . . 8
โข (๐ โ ยฌ (๐โโช dom
๐) โ ๐) |
75 | 8 | sseld 3944 |
. . . . . . . . . 10
โข (๐ โ ((๐โโช dom
๐) โ (๐บ supp โ
) โ (๐โโช dom ๐) โ ๐)) |
76 | | suppssdm 8109 |
. . . . . . . . . . . . . . . 16
โข (๐น supp โ
) โ dom ๐น |
77 | 76, 42 | fssdm 6689 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐น supp โ
) โ ๐ต) |
78 | | onss 7720 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ On โ ๐ต โ On) |
79 | 3, 78 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ On) |
80 | 77, 79 | sstrd 3955 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐น supp โ
) โ On) |
81 | 4 | oif 9471 |
. . . . . . . . . . . . . . . 16
โข ๐:dom ๐โถ(๐น supp โ
) |
82 | 81 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . 15
โข (โช dom ๐ โ dom ๐ โ (๐โโช dom
๐) โ (๐น supp โ
)) |
83 | 62, 82 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โโช dom
๐) โ (๐น supp โ
)) |
84 | 80, 83 | sseldd 3946 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โโช dom
๐) โ
On) |
85 | | eloni 6328 |
. . . . . . . . . . . . 13
โข ((๐โโช dom ๐) โ On โ Ord (๐โโช dom
๐)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ Ord (๐โโช dom
๐)) |
87 | | ordn2lp 6338 |
. . . . . . . . . . . 12
โข (Ord
(๐โโช dom ๐) โ ยฌ ((๐โโช dom
๐) โ ๐ โง ๐ โ (๐โโช dom
๐))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ยฌ ((๐โโช dom
๐) โ ๐ โง ๐ โ (๐โโช dom
๐))) |
89 | | imnan 401 |
. . . . . . . . . . 11
โข (((๐โโช dom ๐) โ ๐ โ ยฌ ๐ โ (๐โโช dom
๐)) โ ยฌ ((๐โโช dom ๐) โ ๐ โง ๐ โ (๐โโช dom
๐))) |
90 | 88, 89 | sylibr 233 |
. . . . . . . . . 10
โข (๐ โ ((๐โโช dom
๐) โ ๐ โ ยฌ ๐ โ (๐โโช dom
๐))) |
91 | 75, 90 | syld 47 |
. . . . . . . . 9
โข (๐ โ ((๐โโช dom
๐) โ (๐บ supp โ
) โ ยฌ
๐ โ (๐โโช dom
๐))) |
92 | | onelon 6343 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ โ ๐ต) โ ๐ โ On) |
93 | 3, 6, 92 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ On) |
94 | | eloni 6328 |
. . . . . . . . . . . 12
โข (๐ โ On โ Ord ๐) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ Ord ๐) |
96 | | ordirr 6336 |
. . . . . . . . . . 11
โข (Ord
๐ โ ยฌ ๐ โ ๐) |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ยฌ ๐ โ ๐) |
98 | | elsni 4604 |
. . . . . . . . . . . 12
โข ((๐โโช dom ๐) โ {๐} โ (๐โโช dom
๐) = ๐) |
99 | 98 | eleq2d 2820 |
. . . . . . . . . . 11
โข ((๐โโช dom ๐) โ {๐} โ (๐ โ (๐โโช dom
๐) โ ๐ โ ๐)) |
100 | 99 | notbid 318 |
. . . . . . . . . 10
โข ((๐โโช dom ๐) โ {๐} โ (ยฌ ๐ โ (๐โโช dom
๐) โ ยฌ ๐ โ ๐)) |
101 | 97, 100 | syl5ibrcom 247 |
. . . . . . . . 9
โข (๐ โ ((๐โโช dom
๐) โ {๐} โ ยฌ ๐ โ (๐โโช dom
๐))) |
102 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ก = ๐ โ (๐ก = ๐ โ ๐ = ๐)) |
103 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
โข (๐ก = ๐ โ (๐บโ๐ก) = (๐บโ๐)) |
104 | 102, 103 | ifbieq2d 4513 |
. . . . . . . . . . . . . 14
โข (๐ก = ๐ โ if(๐ก = ๐, ๐, (๐บโ๐ก)) = if(๐ = ๐, ๐, (๐บโ๐))) |
105 | | eldifi 4087 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ต โ ((๐บ supp โ
) โช {๐})) โ ๐ โ ๐ต) |
106 | 105 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ ๐ โ ๐ต) |
107 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ ๐ โ ๐ด) |
108 | | fvex 6856 |
. . . . . . . . . . . . . . 15
โข (๐บโ๐) โ V |
109 | | ifexg 4536 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ด โง (๐บโ๐) โ V) โ if(๐ = ๐, ๐, (๐บโ๐)) โ V) |
110 | 107, 108,
109 | sylancl 587 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ if(๐ = ๐, ๐, (๐บโ๐)) โ V) |
111 | 9, 104, 106, 110 | fvmptd3 6972 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ (๐นโ๐) = if(๐ = ๐, ๐, (๐บโ๐))) |
112 | | eldifn 4088 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต โ ((๐บ supp โ
) โช {๐})) โ ยฌ ๐ โ ((๐บ supp โ
) โช {๐})) |
113 | 112 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ ยฌ ๐ โ ((๐บ supp โ
) โช {๐})) |
114 | | velsn 4603 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐} โ ๐ = ๐) |
115 | | elun2 4138 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐} โ ๐ โ ((๐บ supp โ
) โช {๐})) |
116 | 114, 115 | sylbir 234 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ๐ โ ((๐บ supp โ
) โช {๐})) |
117 | 113, 116 | nsyl 140 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ ยฌ ๐ = ๐) |
118 | 117 | iffalsed 4498 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ if(๐ = ๐, ๐, (๐บโ๐)) = (๐บโ๐)) |
119 | | ssun1 4133 |
. . . . . . . . . . . . . . . 16
โข (๐บ supp โ
) โ ((๐บ supp โ
) โช {๐}) |
120 | | sscon 4099 |
. . . . . . . . . . . . . . . 16
โข ((๐บ supp โ
) โ ((๐บ supp โ
) โช {๐}) โ (๐ต โ ((๐บ supp โ
) โช {๐})) โ (๐ต โ (๐บ supp โ
))) |
121 | 119, 120 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (๐ต โ ((๐บ supp โ
) โช {๐})) โ (๐ต โ (๐บ supp โ
)) |
122 | 121 | sseli 3941 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ต โ ((๐บ supp โ
) โช {๐})) โ ๐ โ (๐ต โ (๐บ supp โ
))) |
123 | | ssidd 3968 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐บ supp โ
) โ (๐บ supp โ
)) |
124 | 39, 123, 3, 13 | suppssr 8128 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐ต โ (๐บ supp โ
))) โ (๐บโ๐) = โ
) |
125 | 122, 124 | sylan2 594 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ (๐บโ๐) = โ
) |
126 | 111, 118,
125 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐ต โ ((๐บ supp โ
) โช {๐}))) โ (๐นโ๐) = โ
) |
127 | 42, 126 | suppss 8126 |
. . . . . . . . . . 11
โข (๐ โ (๐น supp โ
) โ ((๐บ supp โ
) โช {๐})) |
128 | 127, 83 | sseldd 3946 |
. . . . . . . . . 10
โข (๐ โ (๐โโช dom
๐) โ ((๐บ supp โ
) โช {๐})) |
129 | | elun 4109 |
. . . . . . . . . 10
โข ((๐โโช dom ๐) โ ((๐บ supp โ
) โช {๐}) โ ((๐โโช dom
๐) โ (๐บ supp โ
) โจ (๐โโช dom ๐) โ {๐})) |
130 | 128, 129 | sylib 217 |
. . . . . . . . 9
โข (๐ โ ((๐โโช dom
๐) โ (๐บ supp โ
) โจ (๐โโช dom ๐) โ {๐})) |
131 | 91, 101, 130 | mpjaod 859 |
. . . . . . . 8
โข (๐ โ ยฌ ๐ โ (๐โโช dom
๐)) |
132 | | ioran 983 |
. . . . . . . 8
โข (ยฌ
((๐โโช dom ๐) โ ๐ โจ ๐ โ (๐โโช dom
๐)) โ (ยฌ (๐โโช dom ๐) โ ๐ โง ยฌ ๐ โ (๐โโช dom
๐))) |
133 | 74, 131, 132 | sylanbrc 584 |
. . . . . . 7
โข (๐ โ ยฌ ((๐โโช dom
๐) โ ๐ โจ ๐ โ (๐โโช dom
๐))) |
134 | | ordtri3 6354 |
. . . . . . . 8
โข ((Ord
(๐โโช dom ๐) โง Ord ๐) โ ((๐โโช dom
๐) = ๐ โ ยฌ ((๐โโช dom
๐) โ ๐ โจ ๐ โ (๐โโช dom
๐)))) |
135 | 86, 95, 134 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐โโช dom
๐) = ๐ โ ยฌ ((๐โโช dom
๐) โ ๐ โจ ๐ โ (๐โโช dom
๐)))) |
136 | 133, 135 | mpbird 257 |
. . . . . 6
โข (๐ โ (๐โโช dom
๐) = ๐) |
137 | 136 | oveq2d 7374 |
. . . . 5
โข (๐ โ (๐ด โo (๐โโช dom
๐)) = (๐ด โo ๐)) |
138 | 136 | fveq2d 6847 |
. . . . . 6
โข (๐ โ (๐นโ(๐โโช dom
๐)) = (๐นโ๐)) |
139 | 138, 33 | eqtrd 2773 |
. . . . 5
โข (๐ โ (๐นโ(๐โโช dom
๐)) = ๐) |
140 | 137, 139 | oveq12d 7376 |
. . . 4
โข (๐ โ ((๐ด โo (๐โโช dom
๐)) ยทo
(๐นโ(๐โโช dom
๐))) = ((๐ด โo ๐) ยทo ๐)) |
141 | | nnord 7811 |
. . . . . . . . 9
โข (โช dom ๐ โ ฯ โ Ord โช dom ๐) |
142 | 20, 141 | syl 17 |
. . . . . . . 8
โข (๐ โ Ord โช dom ๐) |
143 | | sssucid 6398 |
. . . . . . . . . 10
โข โช dom ๐ โ suc โช
dom ๐ |
144 | 143, 14 | sseqtrrid 3998 |
. . . . . . . . 9
โข (๐ โ โช dom ๐ โ dom ๐) |
145 | | f1ofo 6792 |
. . . . . . . . . . . . 13
โข (๐:dom ๐โ1-1-ontoโ(๐น supp โ
) โ ๐:dom ๐โontoโ(๐น supp โ
)) |
146 | 28, 145 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐:dom ๐โontoโ(๐น supp โ
)) |
147 | | foima 6762 |
. . . . . . . . . . . 12
โข (๐:dom ๐โontoโ(๐น supp โ
) โ (๐ โ dom ๐) = (๐น supp โ
)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ dom ๐) = (๐น supp โ
)) |
149 | | ffn 6669 |
. . . . . . . . . . . . . 14
โข (๐:dom ๐โถ(๐น supp โ
) โ ๐ Fn dom ๐) |
150 | 81, 149 | ax-mp 5 |
. . . . . . . . . . . . 13
โข ๐ Fn dom ๐ |
151 | | fnsnfv 6921 |
. . . . . . . . . . . . 13
โข ((๐ Fn dom ๐ โง โช dom
๐ โ dom ๐) โ {(๐โโช dom
๐)} = (๐ โ {โช dom
๐})) |
152 | 150, 62, 151 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ {(๐โโช dom
๐)} = (๐ โ {โช dom
๐})) |
153 | 136 | sneqd 4599 |
. . . . . . . . . . . 12
โข (๐ โ {(๐โโช dom
๐)} = {๐}) |
154 | 152, 153 | eqtr3d 2775 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ {โช dom
๐}) = {๐}) |
155 | 148, 154 | difeq12d 4084 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ dom ๐) โ (๐ โ {โช dom
๐})) = ((๐น supp โ
) โ {๐})) |
156 | | ordirr 6336 |
. . . . . . . . . . . . . . . . 17
โข (Ord
โช dom ๐ โ ยฌ โช
dom ๐ โ โช dom ๐) |
157 | 142, 156 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ยฌ โช dom ๐ โ โช dom
๐) |
158 | | disjsn 4673 |
. . . . . . . . . . . . . . . 16
โข ((โช dom ๐ โฉ {โช dom
๐}) = โ
โ ยฌ
โช dom ๐ โ โช dom
๐) |
159 | 157, 158 | sylibr 233 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โช dom ๐ โฉ {โช dom
๐}) =
โ
) |
160 | | disj3 4414 |
. . . . . . . . . . . . . . 15
โข ((โช dom ๐ โฉ {โช dom
๐}) = โ
โ โช dom ๐ = (โช dom ๐ โ {โช dom ๐})) |
161 | 159, 160 | sylib 217 |
. . . . . . . . . . . . . 14
โข (๐ โ โช dom ๐ = (โช dom ๐ โ {โช dom ๐})) |
162 | | difun2 4441 |
. . . . . . . . . . . . . 14
โข ((โช dom ๐ โช {โช dom
๐}) โ {โช dom ๐}) = (โช dom ๐ โ {โช dom ๐}) |
163 | 161, 162 | eqtr4di 2791 |
. . . . . . . . . . . . 13
โข (๐ โ โช dom ๐ = ((โช dom ๐ โช {โช dom ๐}) โ {โช dom
๐})) |
164 | | df-suc 6324 |
. . . . . . . . . . . . . . 15
โข suc โช dom ๐ = (โช dom ๐ โช {โช dom ๐}) |
165 | 14, 164 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
โข (๐ โ dom ๐ = (โช dom ๐ โช {โช dom ๐})) |
166 | 165 | difeq1d 4082 |
. . . . . . . . . . . . 13
โข (๐ โ (dom ๐ โ {โช dom
๐}) = ((โช dom ๐ โช {โช dom
๐}) โ {โช dom ๐})) |
167 | 163, 166 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข (๐ โ โช dom ๐ = (dom ๐ โ {โช dom
๐})) |
168 | 167 | imaeq2d 6014 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โช dom
๐) = (๐ โ (dom ๐ โ {โช dom
๐}))) |
169 | | dff1o3 6791 |
. . . . . . . . . . . . 13
โข (๐:dom ๐โ1-1-ontoโ(๐น supp โ
) โ (๐:dom ๐โontoโ(๐น supp โ
) โง Fun โก๐)) |
170 | 169 | simprbi 498 |
. . . . . . . . . . . 12
โข (๐:dom ๐โ1-1-ontoโ(๐น supp โ
) โ Fun โก๐) |
171 | | imadif 6586 |
. . . . . . . . . . . 12
โข (Fun
โก๐ โ (๐ โ (dom ๐ โ {โช dom
๐})) = ((๐ โ dom ๐) โ (๐ โ {โช dom
๐}))) |
172 | 28, 170, 171 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ (dom ๐ โ {โช dom
๐})) = ((๐ โ dom ๐) โ (๐ โ {โช dom
๐}))) |
173 | 168, 172 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ (๐ โ โช dom
๐) = ((๐ โ dom ๐) โ (๐ โ {โช dom
๐}))) |
174 | 8, 97 | ssneldd 3948 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ ๐ โ (๐บ supp โ
)) |
175 | | disjsn 4673 |
. . . . . . . . . . . . 13
โข (((๐บ supp โ
) โฉ {๐}) = โ
โ ยฌ ๐ โ (๐บ supp โ
)) |
176 | 174, 175 | sylibr 233 |
. . . . . . . . . . . 12
โข (๐ โ ((๐บ supp โ
) โฉ {๐}) = โ
) |
177 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐บโ๐) โ V |
178 | | dif1o 8447 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐บโ๐) โ (V โ 1o) โ
((๐บโ๐) โ V โง (๐บโ๐) โ โ
)) |
179 | 177, 178 | mpbiran 708 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐บโ๐) โ (V โ 1o) โ
(๐บโ๐) โ โ
) |
180 | 39 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ๐บ Fn ๐ต) |
181 | | elsuppfn 8103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐บ Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
182 | 180, 3, 45, 181 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
183 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ((๐บโ๐) โ (V โ 1o) โ
(๐บโ๐) โ โ
)) |
184 | 183 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ((๐บโ๐) โ โ
โ (๐บโ๐) โ (V โ
1o))) |
185 | 184 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
186 | 182, 185 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
187 | 8 | sseld 3944 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โ (๐บ supp โ
) โ ๐ โ ๐)) |
188 | 186, 187 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ (V โ 1o)) โ
๐ โ ๐)) |
189 | 6, 188 | mpand 694 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((๐บโ๐) โ (V โ 1o) โ
๐ โ ๐)) |
190 | 179, 189 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐บโ๐) โ โ
โ ๐ โ ๐)) |
191 | 190 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (ยฌ ๐ โ ๐ โ (๐บโ๐) = โ
)) |
192 | 97, 191 | mpd 15 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บโ๐) = โ
) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (๐บโ๐) = โ
) |
194 | | fveqeq2 6852 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((๐บโ๐) = โ
โ (๐บโ๐) = โ
)) |
195 | 193, 194 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (๐ = ๐ โ (๐บโ๐) = โ
)) |
196 | | eldifi 4087 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ต โ (๐น supp โ
)) โ ๐ โ ๐ต) |
197 | 196 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ ๐ โ ๐ต) |
198 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ ๐ โ ๐ด) |
199 | 198, 108,
109 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ if(๐ = ๐, ๐, (๐บโ๐)) โ V) |
200 | 9, 104, 197, 199 | fvmptd3 6972 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (๐นโ๐) = if(๐ = ๐, ๐, (๐บโ๐))) |
201 | | ssidd 3968 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐น supp โ
) โ (๐น supp โ
)) |
202 | 42, 201, 3, 13 | suppssr 8128 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (๐นโ๐) = โ
) |
203 | 200, 202 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ if(๐ = ๐, ๐, (๐บโ๐)) = โ
) |
204 | | iffalse 4496 |
. . . . . . . . . . . . . . . . 17
โข (ยฌ
๐ = ๐ โ if(๐ = ๐, ๐, (๐บโ๐)) = (๐บโ๐)) |
205 | 204 | eqeq1d 2735 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
๐ = ๐ โ (if(๐ = ๐, ๐, (๐บโ๐)) = โ
โ (๐บโ๐) = โ
)) |
206 | 203, 205 | syl5ibcom 244 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (ยฌ ๐ = ๐ โ (๐บโ๐) = โ
)) |
207 | 195, 206 | pm2.61d 179 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐ต โ (๐น supp โ
))) โ (๐บโ๐) = โ
) |
208 | 39, 207 | suppss 8126 |
. . . . . . . . . . . . 13
โข (๐ โ (๐บ supp โ
) โ (๐น supp โ
)) |
209 | | reldisj 4412 |
. . . . . . . . . . . . 13
โข ((๐บ supp โ
) โ (๐น supp โ
) โ (((๐บ supp โ
) โฉ {๐}) = โ
โ (๐บ supp โ
) โ ((๐น supp โ
) โ {๐}))) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (((๐บ supp โ
) โฉ {๐}) = โ
โ (๐บ supp โ
) โ ((๐น supp โ
) โ {๐}))) |
211 | 176, 210 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ (๐บ supp โ
) โ ((๐น supp โ
) โ {๐})) |
212 | | uncom 4114 |
. . . . . . . . . . . . 13
โข ((๐บ supp โ
) โช {๐}) = ({๐} โช (๐บ supp โ
)) |
213 | 127, 212 | sseqtrdi 3995 |
. . . . . . . . . . . 12
โข (๐ โ (๐น supp โ
) โ ({๐} โช (๐บ supp โ
))) |
214 | | ssundif 4446 |
. . . . . . . . . . . 12
โข ((๐น supp โ
) โ ({๐} โช (๐บ supp โ
)) โ ((๐น supp โ
) โ {๐}) โ (๐บ supp โ
)) |
215 | 213, 214 | sylib 217 |
. . . . . . . . . . 11
โข (๐ โ ((๐น supp โ
) โ {๐}) โ (๐บ supp โ
)) |
216 | 211, 215 | eqssd 3962 |
. . . . . . . . . 10
โข (๐ โ (๐บ supp โ
) = ((๐น supp โ
) โ {๐})) |
217 | 155, 173,
216 | 3eqtr4rd 2784 |
. . . . . . . . 9
โข (๐ โ (๐บ supp โ
) = (๐ โ โช dom
๐)) |
218 | | isores3 7281 |
. . . . . . . . 9
โข ((๐ Isom E , E (dom ๐, (๐น supp โ
)) โง โช dom ๐ โ dom ๐ โง (๐บ supp โ
) = (๐ โ โช dom
๐)) โ (๐ โพ โช dom ๐) Isom E , E (โช
dom ๐, (๐บ supp โ
))) |
219 | 26, 144, 217, 218 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ (๐ โพ โช dom
๐) Isom E , E (โช dom ๐, (๐บ supp โ
))) |
220 | | cantnfp1.k |
. . . . . . . . . . 11
โข ๐พ = OrdIso( E , (๐บ supp โ
)) |
221 | 1, 2, 3, 220, 5 | cantnfcl 9608 |
. . . . . . . . . 10
โข (๐ โ ( E We (๐บ supp โ
) โง dom ๐พ โ ฯ)) |
222 | 221 | simpld 496 |
. . . . . . . . 9
โข (๐ โ E We (๐บ supp โ
)) |
223 | | epse 5617 |
. . . . . . . . 9
โข E Se
(๐บ supp
โ
) |
224 | 220 | oieu 9480 |
. . . . . . . . 9
โข (( E We
(๐บ supp โ
) โง E Se
(๐บ supp โ
)) โ
((Ord โช dom ๐ โง (๐ โพ โช dom
๐) Isom E , E (โช dom ๐, (๐บ supp โ
))) โ (โช dom ๐ = dom ๐พ โง (๐ โพ โช dom
๐) = ๐พ))) |
225 | 222, 223,
224 | sylancl 587 |
. . . . . . . 8
โข (๐ โ ((Ord โช dom ๐ โง (๐ โพ โช dom
๐) Isom E , E (โช dom ๐, (๐บ supp โ
))) โ (โช dom ๐ = dom ๐พ โง (๐ โพ โช dom
๐) = ๐พ))) |
226 | 142, 219,
225 | mpbi2and 711 |
. . . . . . 7
โข (๐ โ (โช dom ๐ = dom ๐พ โง (๐ โพ โช dom
๐) = ๐พ)) |
227 | 226 | simpld 496 |
. . . . . 6
โข (๐ โ โช dom ๐ = dom ๐พ) |
228 | 227 | fveq2d 6847 |
. . . . 5
โข (๐ โ (๐โโช dom
๐) = (๐โdom ๐พ)) |
229 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = โ
โ (๐ฅ โ dom ๐ โ โ
โ dom ๐)) |
230 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = โ
โ (๐ปโ๐ฅ) = (๐ปโโ
)) |
231 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ฅ = โ
โ (๐โ๐ฅ) = (๐โโ
)) |
232 | | cantnfp1.m |
. . . . . . . . . . . . . 14
โข ๐ = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐พโ๐)) ยทo (๐บโ(๐พโ๐))) +o ๐ง)), โ
) |
233 | 232 | seqom0g 8403 |
. . . . . . . . . . . . 13
โข (โ
โ V โ (๐โโ
) = โ
) |
234 | 44, 233 | ax-mp 5 |
. . . . . . . . . . . 12
โข (๐โโ
) =
โ
|
235 | 231, 234 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ฅ = โ
โ (๐โ๐ฅ) = โ
) |
236 | 230, 235 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฅ = โ
โ ((๐ปโ๐ฅ) = (๐โ๐ฅ) โ (๐ปโโ
) = โ
)) |
237 | 229, 236 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = โ
โ ((๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ)) โ (โ
โ dom ๐ โ (๐ปโโ
) =
โ
))) |
238 | 237 | imbi2d 341 |
. . . . . . . 8
โข (๐ฅ = โ
โ ((๐ โ (๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ))) โ (๐ โ (โ
โ dom ๐ โ (๐ปโโ
) =
โ
)))) |
239 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ โ dom ๐ โ ๐ฆ โ dom ๐)) |
240 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ (๐ปโ๐ฅ) = (๐ปโ๐ฆ)) |
241 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ (๐โ๐ฅ) = (๐โ๐ฆ)) |
242 | 240, 241 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ ((๐ปโ๐ฅ) = (๐โ๐ฅ) โ (๐ปโ๐ฆ) = (๐โ๐ฆ))) |
243 | 239, 242 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ ((๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ)) โ (๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ)))) |
244 | 243 | imbi2d 341 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ โ (๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ))) โ (๐ โ (๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ))))) |
245 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = suc ๐ฆ โ (๐ฅ โ dom ๐ โ suc ๐ฆ โ dom ๐)) |
246 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = suc ๐ฆ โ (๐ปโ๐ฅ) = (๐ปโsuc ๐ฆ)) |
247 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = suc ๐ฆ โ (๐โ๐ฅ) = (๐โsuc ๐ฆ)) |
248 | 246, 247 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฅ = suc ๐ฆ โ ((๐ปโ๐ฅ) = (๐โ๐ฅ) โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ))) |
249 | 245, 248 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = suc ๐ฆ โ ((๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ)) โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ)))) |
250 | 249 | imbi2d 341 |
. . . . . . . 8
โข (๐ฅ = suc ๐ฆ โ ((๐ โ (๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ))) โ (๐ โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ))))) |
251 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = โช
dom ๐ โ (๐ฅ โ dom ๐ โ โช dom
๐ โ dom ๐)) |
252 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = โช
dom ๐ โ (๐ปโ๐ฅ) = (๐ปโโช dom
๐)) |
253 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ฅ = โช
dom ๐ โ (๐โ๐ฅ) = (๐โโช dom
๐)) |
254 | 252, 253 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฅ = โช
dom ๐ โ ((๐ปโ๐ฅ) = (๐โ๐ฅ) โ (๐ปโโช dom
๐) = (๐โโช dom
๐))) |
255 | 251, 254 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = โช
dom ๐ โ ((๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ)) โ (โช dom
๐ โ dom ๐ โ (๐ปโโช dom
๐) = (๐โโช dom
๐)))) |
256 | 255 | imbi2d 341 |
. . . . . . . 8
โข (๐ฅ = โช
dom ๐ โ ((๐ โ (๐ฅ โ dom ๐ โ (๐ปโ๐ฅ) = (๐โ๐ฅ))) โ (๐ โ (โช dom
๐ โ dom ๐ โ (๐ปโโช dom
๐) = (๐โโช dom
๐))))) |
257 | 11 | seqom0g 8403 |
. . . . . . . . 9
โข (โ
โ dom ๐ โ (๐ปโโ
) =
โ
) |
258 | 257 | a1i 11 |
. . . . . . . 8
โข (๐ โ (โ
โ dom ๐ โ (๐ปโโ
) = โ
)) |
259 | | nnord 7811 |
. . . . . . . . . . . . . . . 16
โข (dom
๐ โ ฯ โ Ord
dom ๐) |
260 | 17, 259 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ Ord dom ๐) |
261 | | ordtr 6332 |
. . . . . . . . . . . . . . 15
โข (Ord dom
๐ โ Tr dom ๐) |
262 | 260, 261 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ Tr dom ๐) |
263 | | trsuc 6405 |
. . . . . . . . . . . . . 14
โข ((Tr dom
๐ โง suc ๐ฆ โ dom ๐) โ ๐ฆ โ dom ๐) |
264 | 262, 263 | sylan 581 |
. . . . . . . . . . . . 13
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ๐ฆ โ dom ๐) |
265 | 264 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (suc ๐ฆ โ dom ๐ โ ๐ฆ โ dom ๐)) |
266 | 265 | imim1d 82 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ)) โ (suc ๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ)))) |
267 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข ((๐ปโ๐ฆ) = (๐โ๐ฆ) โ (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐ปโ๐ฆ)) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐โ๐ฆ))) |
268 | | elnn 7814 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ dom ๐ โง dom ๐ โ ฯ) โ ๐ฆ โ ฯ) |
269 | 268 | ancoms 460 |
. . . . . . . . . . . . . . . . 17
โข ((dom
๐ โ ฯ โง
๐ฆ โ dom ๐) โ ๐ฆ โ ฯ) |
270 | 17, 264, 269 | syl2an2r 684 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ๐ฆ โ ฯ) |
271 | 1, 2, 3, 4, 10, 11 | cantnfsuc 9611 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ ฯ) โ (๐ปโsuc ๐ฆ) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐ปโ๐ฆ))) |
272 | 270, 271 | syldan 592 |
. . . . . . . . . . . . . . 15
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐ปโsuc ๐ฆ) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐ปโ๐ฆ))) |
273 | 1, 2, 3, 220, 5, 232 | cantnfsuc 9611 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฆ โ ฯ) โ (๐โsuc ๐ฆ) = (((๐ด โo (๐พโ๐ฆ)) ยทo (๐บโ(๐พโ๐ฆ))) +o (๐โ๐ฆ))) |
274 | 270, 273 | syldan 592 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐โsuc ๐ฆ) = (((๐ด โo (๐พโ๐ฆ)) ยทo (๐บโ(๐พโ๐ฆ))) +o (๐โ๐ฆ))) |
275 | 226 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โพ โช dom
๐) = ๐พ) |
276 | 275 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ โพ โช dom
๐)โ๐ฆ) = (๐พโ๐ฆ)) |
277 | 276 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ((๐ โพ โช dom
๐)โ๐ฆ) = (๐พโ๐ฆ)) |
278 | 14 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (suc ๐ฆ โ dom ๐ โ suc ๐ฆ โ suc โช dom
๐)) |
279 | 278 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง suc ๐ฆ โ dom ๐) โ suc ๐ฆ โ suc โช dom
๐) |
280 | 142 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง suc ๐ฆ โ dom ๐) โ Ord โช
dom ๐) |
281 | | ordsucelsuc 7758 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (Ord
โช dom ๐ โ (๐ฆ โ โช dom
๐ โ suc ๐ฆ โ suc โช dom ๐)) |
282 | 280, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐ฆ โ โช dom
๐ โ suc ๐ฆ โ suc โช dom ๐)) |
283 | 279, 282 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ๐ฆ โ โช dom
๐) |
284 | 283 | fvresd 6863 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ((๐ โพ โช dom
๐)โ๐ฆ) = (๐โ๐ฆ)) |
285 | 277, 284 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐พโ๐ฆ) = (๐โ๐ฆ)) |
286 | 285 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐ด โo (๐พโ๐ฆ)) = (๐ด โo (๐โ๐ฆ))) |
287 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ก = (๐พโ๐ฆ) โ (๐ก = ๐ โ (๐พโ๐ฆ) = ๐)) |
288 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ก = (๐พโ๐ฆ) โ (๐บโ๐ก) = (๐บโ(๐พโ๐ฆ))) |
289 | 287, 288 | ifbieq2d 4513 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก = (๐พโ๐ฆ) โ if(๐ก = ๐, ๐, (๐บโ๐ก)) = if((๐พโ๐ฆ) = ๐, ๐, (๐บโ(๐พโ๐ฆ)))) |
290 | | suppssdm 8109 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐บ supp โ
) โ dom ๐บ |
291 | 290, 39 | fssdm 6689 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐บ supp โ
) โ ๐ต) |
292 | 291 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐บ supp โ
) โ ๐ต) |
293 | 227 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง suc ๐ฆ โ dom ๐) โ โช dom
๐ = dom ๐พ) |
294 | 283, 293 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ๐ฆ โ dom ๐พ) |
295 | 220 | oif 9471 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐พ:dom ๐พโถ(๐บ supp โ
) |
296 | 295 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ dom ๐พ โ (๐พโ๐ฆ) โ (๐บ supp โ
)) |
297 | 294, 296 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐พโ๐ฆ) โ (๐บ supp โ
)) |
298 | 292, 297 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐พโ๐ฆ) โ ๐ต) |
299 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ๐ โ ๐ด) |
300 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐บโ(๐พโ๐ฆ)) โ V |
301 | | ifexg 4536 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ ๐ด โง (๐บโ(๐พโ๐ฆ)) โ V) โ if((๐พโ๐ฆ) = ๐, ๐, (๐บโ(๐พโ๐ฆ))) โ V) |
302 | 299, 300,
301 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง suc ๐ฆ โ dom ๐) โ if((๐พโ๐ฆ) = ๐, ๐, (๐บโ(๐พโ๐ฆ))) โ V) |
303 | 9, 289, 298, 302 | fvmptd3 6972 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐นโ(๐พโ๐ฆ)) = if((๐พโ๐ฆ) = ๐, ๐, (๐บโ(๐พโ๐ฆ)))) |
304 | 285 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐นโ(๐พโ๐ฆ)) = (๐นโ(๐โ๐ฆ))) |
305 | 174 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ยฌ ๐ โ (๐บ supp โ
)) |
306 | | nelneq 2858 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐พโ๐ฆ) โ (๐บ supp โ
) โง ยฌ ๐ โ (๐บ supp โ
)) โ ยฌ (๐พโ๐ฆ) = ๐) |
307 | 297, 305,
306 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ยฌ (๐พโ๐ฆ) = ๐) |
308 | 307 | iffalsed 4498 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง suc ๐ฆ โ dom ๐) โ if((๐พโ๐ฆ) = ๐, ๐, (๐บโ(๐พโ๐ฆ))) = (๐บโ(๐พโ๐ฆ))) |
309 | 303, 304,
308 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐บโ(๐พโ๐ฆ)) = (๐นโ(๐โ๐ฆ))) |
310 | 286, 309 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ((๐ด โo (๐พโ๐ฆ)) ยทo (๐บโ(๐พโ๐ฆ))) = ((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ)))) |
311 | 310 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (((๐ด โo (๐พโ๐ฆ)) ยทo (๐บโ(๐พโ๐ฆ))) +o (๐โ๐ฆ)) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐โ๐ฆ))) |
312 | 274, 311 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข ((๐ โง suc ๐ฆ โ dom ๐) โ (๐โsuc ๐ฆ) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐โ๐ฆ))) |
313 | 272, 312 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ((๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ) โ (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐ปโ๐ฆ)) = (((๐ด โo (๐โ๐ฆ)) ยทo (๐นโ(๐โ๐ฆ))) +o (๐โ๐ฆ)))) |
314 | 267, 313 | imbitrrid 245 |
. . . . . . . . . . . . 13
โข ((๐ โง suc ๐ฆ โ dom ๐) โ ((๐ปโ๐ฆ) = (๐โ๐ฆ) โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ))) |
315 | 314 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (suc ๐ฆ โ dom ๐ โ ((๐ปโ๐ฆ) = (๐โ๐ฆ) โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ)))) |
316 | 315 | a2d 29 |
. . . . . . . . . . 11
โข (๐ โ ((suc ๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ)) โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ)))) |
317 | 266, 316 | syld 47 |
. . . . . . . . . 10
โข (๐ โ ((๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ)) โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ)))) |
318 | 317 | a2i 14 |
. . . . . . . . 9
โข ((๐ โ (๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ))) โ (๐ โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ)))) |
319 | 318 | a1i 11 |
. . . . . . . 8
โข (๐ฆ โ ฯ โ ((๐ โ (๐ฆ โ dom ๐ โ (๐ปโ๐ฆ) = (๐โ๐ฆ))) โ (๐ โ (suc ๐ฆ โ dom ๐ โ (๐ปโsuc ๐ฆ) = (๐โsuc ๐ฆ))))) |
320 | 238, 244,
250, 256, 258, 319 | finds 7836 |
. . . . . . 7
โข (โช dom ๐ โ ฯ โ (๐ โ (โช dom
๐ โ dom ๐ โ (๐ปโโช dom
๐) = (๐โโช dom
๐)))) |
321 | 20, 320 | mpcom 38 |
. . . . . 6
โข (๐ โ (โช dom ๐ โ dom ๐ โ (๐ปโโช dom
๐) = (๐โโช dom
๐))) |
322 | 62, 321 | mpd 15 |
. . . . 5
โข (๐ โ (๐ปโโช dom
๐) = (๐โโช dom
๐)) |
323 | 1, 2, 3, 220, 5, 232 | cantnfval 9609 |
. . . . 5
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) = (๐โdom ๐พ)) |
324 | 228, 322,
323 | 3eqtr4d 2783 |
. . . 4
โข (๐ โ (๐ปโโช dom
๐) = ((๐ด CNF ๐ต)โ๐บ)) |
325 | 140, 324 | oveq12d 7376 |
. . 3
โข (๐ โ (((๐ด โo (๐โโช dom
๐)) ยทo
(๐นโ(๐โโช dom
๐))) +o (๐ปโโช dom ๐)) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
326 | 22, 325 | eqtrd 2773 |
. 2
โข (๐ โ (๐ปโsuc โช dom
๐) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
327 | 12, 15, 326 | 3eqtrd 2777 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |