Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . 3
โข ((๐นโ๐ถ) = โ
โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) = ((๐ด โo ๐ถ) ยทo
โ
)) |
2 | 1 | sseq1d 3979 |
. 2
โข ((๐นโ๐ถ) = โ
โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ ((๐ด CNF ๐ต)โ๐น) โ ((๐ด โo ๐ถ) ยทo โ
) โ
((๐ด CNF ๐ต)โ๐น))) |
3 | | ovexd 7396 |
. . . . . . . . 9
โข (๐ โ (๐น supp โ
) โ V) |
4 | | cantnfs.s |
. . . . . . . . . . 11
โข ๐ = dom (๐ด CNF ๐ต) |
5 | | cantnfs.a |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ On) |
6 | | cantnfs.b |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ On) |
7 | | cantnfcl.g |
. . . . . . . . . . 11
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
8 | | cantnfcl.f |
. . . . . . . . . . 11
โข (๐ โ ๐น โ ๐) |
9 | 4, 5, 6, 7, 8 | cantnfcl 9611 |
. . . . . . . . . 10
โข (๐ โ ( E We (๐น supp โ
) โง dom ๐บ โ ฯ)) |
10 | 9 | simpld 496 |
. . . . . . . . 9
โข (๐ โ E We (๐น supp โ
)) |
11 | 7 | oiiso 9481 |
. . . . . . . . 9
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
12 | 3, 10, 11 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
13 | | isof1o 7272 |
. . . . . . . 8
โข (๐บ Isom E , E (dom ๐บ, (๐น supp โ
)) โ ๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
โข (๐ โ ๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
)) |
15 | 14 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
)) |
16 | | f1ocnv 6800 |
. . . . . 6
โข (๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
) โ โก๐บ:(๐น supp โ
)โ1-1-ontoโdom
๐บ) |
17 | | f1of 6788 |
. . . . . 6
โข (โก๐บ:(๐น supp โ
)โ1-1-ontoโdom
๐บ โ โก๐บ:(๐น supp โ
)โถdom ๐บ) |
18 | 15, 16, 17 | 3syl 18 |
. . . . 5
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ โก๐บ:(๐น supp โ
)โถdom ๐บ) |
19 | | cantnfle.c |
. . . . . . 7
โข (๐ โ ๐ถ โ ๐ต) |
20 | 19 | anim1i 616 |
. . . . . 6
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ (๐ถ โ ๐ต โง (๐นโ๐ถ) โ โ
)) |
21 | 4, 5, 6 | cantnfs 9610 |
. . . . . . . . . . 11
โข (๐ โ (๐น โ ๐ โ (๐น:๐ตโถ๐ด โง ๐น finSupp โ
))) |
22 | 8, 21 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐น:๐ตโถ๐ด โง ๐น finSupp โ
)) |
23 | 22 | simpld 496 |
. . . . . . . . 9
โข (๐ โ ๐น:๐ตโถ๐ด) |
24 | 23 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ๐น:๐ตโถ๐ด) |
25 | 24 | ffnd 6673 |
. . . . . . 7
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ๐น Fn ๐ต) |
26 | 6 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ๐ต โ On) |
27 | | 0ex 5268 |
. . . . . . . 8
โข โ
โ V |
28 | 27 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ โ
โ
V) |
29 | | elsuppfn 8106 |
. . . . . . 7
โข ((๐น Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ถ โ (๐น supp โ
) โ (๐ถ โ ๐ต โง (๐นโ๐ถ) โ โ
))) |
30 | 25, 26, 28, 29 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ (๐ถ โ (๐น supp โ
) โ (๐ถ โ ๐ต โง (๐นโ๐ถ) โ โ
))) |
31 | 20, 30 | mpbird 257 |
. . . . 5
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ๐ถ โ (๐น supp โ
)) |
32 | 18, 31 | ffvelcdmd 7040 |
. . . 4
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ (โก๐บโ๐ถ) โ dom ๐บ) |
33 | 9 | simprd 497 |
. . . . . 6
โข (๐ โ dom ๐บ โ ฯ) |
34 | 33 | adantr 482 |
. . . . 5
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ dom ๐บ โ ฯ) |
35 | | eqimss 4004 |
. . . . . . . . . 10
โข (๐ฅ = dom ๐บ โ ๐ฅ โ dom ๐บ) |
36 | 35 | biantrurd 534 |
. . . . . . . . 9
โข (๐ฅ = dom ๐บ โ ((โก๐บโ๐ถ) โ ๐ฅ โ (๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ))) |
37 | | eleq2 2823 |
. . . . . . . . 9
โข (๐ฅ = dom ๐บ โ ((โก๐บโ๐ถ) โ ๐ฅ โ (โก๐บโ๐ถ) โ dom ๐บ)) |
38 | 36, 37 | bitr3d 281 |
. . . . . . . 8
โข (๐ฅ = dom ๐บ โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ (โก๐บโ๐ถ) โ dom ๐บ)) |
39 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = dom ๐บ โ (๐ปโ๐ฅ) = (๐ปโdom ๐บ)) |
40 | 39 | sseq2d 3980 |
. . . . . . . 8
โข (๐ฅ = dom ๐บ โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ))) |
41 | 38, 40 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = dom ๐บ โ (((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ)) โ ((โก๐บโ๐ถ) โ dom ๐บ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ)))) |
42 | 41 | imbi2d 341 |
. . . . . 6
โข (๐ฅ = dom ๐บ โ (((๐ โง (๐นโ๐ถ) โ โ
) โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ))) โ ((๐ โง (๐นโ๐ถ) โ โ
) โ ((โก๐บโ๐ถ) โ dom ๐บ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ))))) |
43 | | sseq1 3973 |
. . . . . . . . 9
โข (๐ฅ = โ
โ (๐ฅ โ dom ๐บ โ โ
โ dom ๐บ)) |
44 | | eleq2 2823 |
. . . . . . . . 9
โข (๐ฅ = โ
โ ((โก๐บโ๐ถ) โ ๐ฅ โ (โก๐บโ๐ถ) โ โ
)) |
45 | 43, 44 | anbi12d 632 |
. . . . . . . 8
โข (๐ฅ = โ
โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ (โ
โ dom ๐บ โง (โก๐บโ๐ถ) โ โ
))) |
46 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = โ
โ (๐ปโ๐ฅ) = (๐ปโโ
)) |
47 | 46 | sseq2d 3980 |
. . . . . . . 8
โข (๐ฅ = โ
โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโโ
))) |
48 | 45, 47 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = โ
โ (((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ)) โ ((โ
โ dom ๐บ โง (โก๐บโ๐ถ) โ โ
) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโโ
)))) |
49 | | sseq1 3973 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ฅ โ dom ๐บ โ ๐ฆ โ dom ๐บ)) |
50 | | eleq2 2823 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ ((โก๐บโ๐ถ) โ ๐ฅ โ (โก๐บโ๐ถ) โ ๐ฆ)) |
51 | 49, 50 | anbi12d 632 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ (๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ))) |
52 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ปโ๐ฅ) = (๐ปโ๐ฆ)) |
53 | 52 | sseq2d 3980 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ))) |
54 | 51, 53 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ)) โ ((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)))) |
55 | | sseq1 3973 |
. . . . . . . . 9
โข (๐ฅ = suc ๐ฆ โ (๐ฅ โ dom ๐บ โ suc ๐ฆ โ dom ๐บ)) |
56 | | eleq2 2823 |
. . . . . . . . 9
โข (๐ฅ = suc ๐ฆ โ ((โก๐บโ๐ถ) โ ๐ฅ โ (โก๐บโ๐ถ) โ suc ๐ฆ)) |
57 | 55, 56 | anbi12d 632 |
. . . . . . . 8
โข (๐ฅ = suc ๐ฆ โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ suc ๐ฆ))) |
58 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = suc ๐ฆ โ (๐ปโ๐ฅ) = (๐ปโsuc ๐ฆ)) |
59 | 58 | sseq2d 3980 |
. . . . . . . 8
โข (๐ฅ = suc ๐ฆ โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
60 | 57, 59 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = suc ๐ฆ โ (((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ)) โ ((suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ suc ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
61 | | noel 4294 |
. . . . . . . . . 10
โข ยฌ
(โก๐บโ๐ถ) โ โ
|
62 | 61 | pm2.21i 119 |
. . . . . . . . 9
โข ((โก๐บโ๐ถ) โ โ
โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโโ
)) |
63 | 62 | adantl 483 |
. . . . . . . 8
โข ((โ
โ dom ๐บ โง (โก๐บโ๐ถ) โ โ
) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโโ
)) |
64 | 63 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ((โ
โ dom
๐บ โง (โก๐บโ๐ถ) โ โ
) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโโ
))) |
65 | | fvex 6859 |
. . . . . . . . . . . 12
โข (โก๐บโ๐ถ) โ V |
66 | 65 | elsuc 6391 |
. . . . . . . . . . 11
โข ((โก๐บโ๐ถ) โ suc ๐ฆ โ ((โก๐บโ๐ถ) โ ๐ฆ โจ (โก๐บโ๐ถ) = ๐ฆ)) |
67 | | sssucid 6401 |
. . . . . . . . . . . . . . . . 17
โข ๐ฆ โ suc ๐ฆ |
68 | | sstr 3956 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ suc ๐ฆ โง suc ๐ฆ โ dom ๐บ) โ ๐ฆ โ dom ๐บ) |
69 | 67, 68 | mpan 689 |
. . . . . . . . . . . . . . . 16
โข (suc
๐ฆ โ dom ๐บ โ ๐ฆ โ dom ๐บ) |
70 | 69 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ)) โ ๐ฆ โ dom ๐บ) |
71 | | simprr 772 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ)) โ (โก๐บโ๐ถ) โ ๐ฆ) |
72 | | pm2.27 42 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ))) |
73 | 70, 71, 72 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ)) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ))) |
74 | | cantnfval.h |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
75 | 74 | cantnfvalf 9609 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ป:ฯโถOn |
76 | 75 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ ฯ โ (๐ปโ๐ฆ) โ On) |
77 | 76 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐ปโ๐ฆ) โ On) |
78 | 5 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ๐ด โ On) |
79 | 6 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ๐ต โ On) |
80 | | suppssdm 8112 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐น supp โ
) โ dom ๐น |
81 | 80, 23 | fssdm 6692 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐น supp โ
) โ ๐ต) |
82 | 81 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐น supp โ
) โ ๐ต) |
83 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ suc ๐ฆ โ dom ๐บ) |
84 | | sucidg 6402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ ฯ โ ๐ฆ โ suc ๐ฆ) |
85 | 84 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ๐ฆ โ suc ๐ฆ) |
86 | 83, 85 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ๐ฆ โ dom ๐บ) |
87 | 7 | oif 9474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ๐บ:dom ๐บโถ(๐น supp โ
) |
88 | 87 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ dom ๐บ โ (๐บโ๐ฆ) โ (๐น supp โ
)) |
89 | 86, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐บโ๐ฆ) โ (๐น supp โ
)) |
90 | 82, 89 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐บโ๐ฆ) โ ๐ต) |
91 | | onelon 6346 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ On โง (๐บโ๐ฆ) โ ๐ต) โ (๐บโ๐ฆ) โ On) |
92 | 79, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐บโ๐ฆ) โ On) |
93 | | oecl 8487 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ On โง (๐บโ๐ฆ) โ On) โ (๐ด โo (๐บโ๐ฆ)) โ On) |
94 | 78, 92, 93 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐ด โo (๐บโ๐ฆ)) โ On) |
95 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ๐น:๐ตโถ๐ด) |
96 | 95, 90 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐นโ(๐บโ๐ฆ)) โ ๐ด) |
97 | | onelon 6346 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ On โง (๐นโ(๐บโ๐ฆ)) โ ๐ด) โ (๐นโ(๐บโ๐ฆ)) โ On) |
98 | 78, 96, 97 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐นโ(๐บโ๐ฆ)) โ On) |
99 | | omcl 8486 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โo (๐บโ๐ฆ)) โ On โง (๐นโ(๐บโ๐ฆ)) โ On) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ On) |
100 | 94, 98, 99 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ On) |
101 | | oaword2 8504 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ปโ๐ฆ) โ On โง ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ On) โ (๐ปโ๐ฆ) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
102 | 77, 100, 101 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐ปโ๐ฆ) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
103 | 4, 5, 6, 7, 8, 74 | cantnfsuc 9614 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฆ โ ฯ) โ (๐ปโsuc ๐ฆ) = (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
104 | 103 | ad4ant13 750 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐ปโsuc ๐ฆ) = (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
105 | 102, 104 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (๐ปโ๐ฆ) โ (๐ปโsuc ๐ฆ)) |
106 | | sstr 3956 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ) โง (๐ปโ๐ฆ) โ (๐ปโsuc ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)) |
107 | 106 | expcom 415 |
. . . . . . . . . . . . . . . 16
โข ((๐ปโ๐ฆ) โ (๐ปโsuc ๐ฆ) โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
108 | 105, 107 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
109 | 108 | adantrr 716 |
. . . . . . . . . . . . . 14
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ)) โ (((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
110 | 73, 109 | syld 47 |
. . . . . . . . . . . . 13
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ)) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
111 | 110 | expr 458 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((โก๐บโ๐ถ) โ ๐ฆ โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
112 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (โก๐บโ๐ถ) = ๐ฆ) |
113 | 112 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐บโ(โก๐บโ๐ถ)) = (๐บโ๐ฆ)) |
114 | | f1ocnvfv2 7227 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐บ:dom ๐บโ1-1-ontoโ(๐น supp โ
) โง ๐ถ โ (๐น supp โ
)) โ (๐บโ(โก๐บโ๐ถ)) = ๐ถ) |
115 | 15, 31, 114 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ (๐บโ(โก๐บโ๐ถ)) = ๐ถ) |
116 | 115 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐บโ(โก๐บโ๐ถ)) = ๐ถ) |
117 | 113, 116 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐บโ๐ฆ) = ๐ถ) |
118 | 117 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐ด โo (๐บโ๐ฆ)) = (๐ด โo ๐ถ)) |
119 | 117 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐นโ(๐บโ๐ฆ)) = (๐นโ๐ถ)) |
120 | 118, 119 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) = ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ))) |
121 | | oaword1 8503 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ On โง (๐ปโ๐ฆ) โ On) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
122 | 100, 77, 121 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
123 | 122 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ ((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
124 | 120, 123 | eqsstrrd 3987 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
125 | 103 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ (๐ปโsuc ๐ฆ) = (((๐ด โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) +o (๐ปโ๐ฆ))) |
126 | 124, 125 | sseqtrrd 3989 |
. . . . . . . . . . . . . 14
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) = ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)) |
127 | 126 | expr 458 |
. . . . . . . . . . . . 13
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((โก๐บโ๐ถ) = ๐ฆ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))) |
128 | 127 | a1dd 50 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((โก๐บโ๐ถ) = ๐ฆ โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
129 | 111, 128 | jaod 858 |
. . . . . . . . . . 11
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ (((โก๐บโ๐ถ) โ ๐ฆ โจ (โก๐บโ๐ถ) = ๐ฆ) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
130 | 66, 129 | biimtrid 241 |
. . . . . . . . . 10
โข ((((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โง suc ๐ฆ โ dom ๐บ) โ ((โก๐บโ๐ถ) โ suc ๐ฆ โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
131 | 130 | expimpd 455 |
. . . . . . . . 9
โข (((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โ ((suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ suc ๐ฆ) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
132 | 131 | com23 86 |
. . . . . . . 8
โข (((๐ โง (๐นโ๐ถ) โ โ
) โง ๐ฆ โ ฯ) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ suc ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ)))) |
133 | 132 | expcom 415 |
. . . . . . 7
โข (๐ฆ โ ฯ โ ((๐ โง (๐นโ๐ถ) โ โ
) โ (((๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฆ)) โ ((suc ๐ฆ โ dom ๐บ โง (โก๐บโ๐ถ) โ suc ๐ฆ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโsuc ๐ฆ))))) |
134 | 48, 54, 60, 64, 133 | finds2 7841 |
. . . . . 6
โข (๐ฅ โ ฯ โ ((๐ โง (๐นโ๐ถ) โ โ
) โ ((๐ฅ โ dom ๐บ โง (โก๐บโ๐ถ) โ ๐ฅ) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโ๐ฅ)))) |
135 | 42, 134 | vtoclga 3536 |
. . . . 5
โข (dom
๐บ โ ฯ โ
((๐ โง (๐นโ๐ถ) โ โ
) โ ((โก๐บโ๐ถ) โ dom ๐บ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ)))) |
136 | 34, 135 | mpcom 38 |
. . . 4
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ((โก๐บโ๐ถ) โ dom ๐บ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ))) |
137 | 32, 136 | mpd 15 |
. . 3
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ (๐ปโdom ๐บ)) |
138 | 4, 5, 6, 7, 8, 74 | cantnfval 9612 |
. . . 4
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (๐ปโdom ๐บ)) |
139 | 138 | adantr 482 |
. . 3
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ((๐ด CNF ๐ต)โ๐น) = (๐ปโdom ๐บ)) |
140 | 137, 139 | sseqtrrd 3989 |
. 2
โข ((๐ โง (๐นโ๐ถ) โ โ
) โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ ((๐ด CNF ๐ต)โ๐น)) |
141 | | onelon 6346 |
. . . . . 6
โข ((๐ต โ On โง ๐ถ โ ๐ต) โ ๐ถ โ On) |
142 | 6, 19, 141 | syl2anc 585 |
. . . . 5
โข (๐ โ ๐ถ โ On) |
143 | | oecl 8487 |
. . . . 5
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด โo ๐ถ) โ On) |
144 | 5, 142, 143 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ด โo ๐ถ) โ On) |
145 | | om0 8467 |
. . . 4
โข ((๐ด โo ๐ถ) โ On โ ((๐ด โo ๐ถ) ยทo โ
)
= โ
) |
146 | 144, 145 | syl 17 |
. . 3
โข (๐ โ ((๐ด โo ๐ถ) ยทo โ
) =
โ
) |
147 | | 0ss 4360 |
. . 3
โข โ
โ ((๐ด CNF ๐ต)โ๐น) |
148 | 146, 147 | eqsstrdi 4002 |
. 2
โข (๐ โ ((๐ด โo ๐ถ) ยทo โ
) โ
((๐ด CNF ๐ต)โ๐น)) |
149 | 2, 140, 148 | pm2.61ne 3027 |
1
โข (๐ โ ((๐ด โo ๐ถ) ยทo (๐นโ๐ถ)) โ ((๐ด CNF ๐ต)โ๐น)) |