Step | Hyp | Ref
| Expression |
1 | | cantnfp1.f |
. . . . . 6
โข ๐น = (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) |
2 | | cantnfs.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ On) |
3 | | cantnfp1.x |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐ต) |
4 | | onelon 6346 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ โ ๐ต) โ ๐ โ On) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ On) |
6 | | eloni 6331 |
. . . . . . . . . . . 12
โข (๐ โ On โ Ord ๐) |
7 | | ordirr 6339 |
. . . . . . . . . . . 12
โข (Ord
๐ โ ยฌ ๐ โ ๐) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ ยฌ ๐ โ ๐) |
9 | | fvex 6859 |
. . . . . . . . . . . . . 14
โข (๐บโ๐) โ V |
10 | | dif1o 8450 |
. . . . . . . . . . . . . 14
โข ((๐บโ๐) โ (V โ 1o) โ
((๐บโ๐) โ V โง (๐บโ๐) โ โ
)) |
11 | 9, 10 | mpbiran 708 |
. . . . . . . . . . . . 13
โข ((๐บโ๐) โ (V โ 1o) โ
(๐บโ๐) โ โ
) |
12 | | cantnfp1.g |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐บ โ ๐) |
13 | | cantnfs.s |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ = dom (๐ด CNF ๐ต) |
14 | | cantnfs.a |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ด โ On) |
15 | 13, 14, 2 | cantnfs 9610 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ โ ๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
))) |
16 | 12, 15 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
)) |
17 | 16 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บ:๐ตโถ๐ด) |
18 | 17 | ffnd 6673 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐บ Fn ๐ต) |
19 | | 0ex 5268 |
. . . . . . . . . . . . . . . . . 18
โข โ
โ V |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ
โ
V) |
21 | | elsuppfn 8106 |
. . . . . . . . . . . . . . . . 17
โข ((๐บ Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
22 | 18, 2, 20, 21 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
23 | 11 | bicomi 223 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บโ๐) โ โ
โ (๐บโ๐) โ (V โ
1o)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐บโ๐) โ โ
โ (๐บโ๐) โ (V โ
1o))) |
25 | 24 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
26 | 22, 25 | bitrd 279 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
27 | | cantnfp1.s |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐บ supp โ
) โ ๐) |
28 | 27 | sseld 3947 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ (๐บ supp โ
) โ ๐ โ ๐)) |
29 | 26, 28 | sylbird 260 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ (V โ 1o)) โ
๐ โ ๐)) |
30 | 3, 29 | mpand 694 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐บโ๐) โ (V โ 1o) โ
๐ โ ๐)) |
31 | 11, 30 | biimtrrid 242 |
. . . . . . . . . . . 12
โข (๐ โ ((๐บโ๐) โ โ
โ ๐ โ ๐)) |
32 | 31 | necon1bd 2958 |
. . . . . . . . . . 11
โข (๐ โ (ยฌ ๐ โ ๐ โ (๐บโ๐) = โ
)) |
33 | 8, 32 | mpd 15 |
. . . . . . . . . 10
โข (๐ โ (๐บโ๐) = โ
) |
34 | 33 | ad3antrrr 729 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ (๐บโ๐) = โ
) |
35 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ก = ๐) |
36 | 35 | fveq2d 6850 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ (๐บโ๐ก) = (๐บโ๐)) |
37 | | simpllr 775 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ = โ
) |
38 | 34, 36, 37 | 3eqtr4rd 2784 |
. . . . . . . 8
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ = (๐บโ๐ก)) |
39 | | eqidd 2734 |
. . . . . . . 8
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ยฌ ๐ก = ๐) โ (๐บโ๐ก) = (๐บโ๐ก)) |
40 | 38, 39 | ifeqda 4526 |
. . . . . . 7
โข (((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โ if(๐ก = ๐, ๐, (๐บโ๐ก)) = (๐บโ๐ก)) |
41 | 40 | mpteq2dva 5209 |
. . . . . 6
โข ((๐ โง ๐ = โ
) โ (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
42 | 1, 41 | eqtrid 2785 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ๐น = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
43 | 17 | feqmptd 6914 |
. . . . . 6
โข (๐ โ ๐บ = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
44 | 43 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ๐บ = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
45 | 42, 44 | eqtr4d 2776 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ๐น = ๐บ) |
46 | 12 | adantr 482 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ๐บ โ ๐) |
47 | 45, 46 | eqeltrd 2834 |
. . 3
โข ((๐ โง ๐ = โ
) โ ๐น โ ๐) |
48 | | oecl 8487 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
49 | 14, 2, 48 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐ต) โ On) |
50 | 13, 14, 2 | cantnff 9618 |
. . . . . . . 8
โข (๐ โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
51 | 50, 12 | ffvelcdmd 7040 |
. . . . . . 7
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) โ (๐ด โo ๐ต)) |
52 | | onelon 6346 |
. . . . . . 7
โข (((๐ด โo ๐ต) โ On โง ((๐ด CNF ๐ต)โ๐บ) โ (๐ด โo ๐ต)) โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
53 | 49, 51, 52 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
54 | 53 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
55 | | oa0r 8488 |
. . . . 5
โข (((๐ด CNF ๐ต)โ๐บ) โ On โ (โ
+o
((๐ด CNF ๐ต)โ๐บ)) = ((๐ด CNF ๐ต)โ๐บ)) |
56 | 54, 55 | syl 17 |
. . . 4
โข ((๐ โง ๐ = โ
) โ (โ
+o
((๐ด CNF ๐ต)โ๐บ)) = ((๐ด CNF ๐ต)โ๐บ)) |
57 | | oveq2 7369 |
. . . . . 6
โข (๐ = โ
โ ((๐ด โo ๐) ยทo ๐) = ((๐ด โo ๐) ยทo
โ
)) |
58 | | oecl 8487 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ โ On) โ (๐ด โo ๐) โ On) |
59 | 14, 5, 58 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐) โ On) |
60 | | om0 8467 |
. . . . . . 7
โข ((๐ด โo ๐) โ On โ ((๐ด โo ๐) ยทo โ
)
= โ
) |
61 | 59, 60 | syl 17 |
. . . . . 6
โข (๐ โ ((๐ด โo ๐) ยทo โ
) =
โ
) |
62 | 57, 61 | sylan9eqr 2795 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ((๐ด โo ๐) ยทo ๐) = โ
) |
63 | 62 | oveq1d 7376 |
. . . 4
โข ((๐ โง ๐ = โ
) โ (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)) = (โ
+o ((๐ด CNF ๐ต)โ๐บ))) |
64 | 45 | fveq2d 6850 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐น) = ((๐ด CNF ๐ต)โ๐บ)) |
65 | 56, 63, 64 | 3eqtr4rd 2784 |
. . 3
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
66 | 47, 65 | jca 513 |
. 2
โข ((๐ โง ๐ = โ
) โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |
67 | 14 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ด โ On) |
68 | 2 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ต โ On) |
69 | 12 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐บ โ ๐) |
70 | 3 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ โ ๐ต) |
71 | | cantnfp1.y |
. . . . 5
โข (๐ โ ๐ โ ๐ด) |
72 | 71 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ โ ๐ด) |
73 | 27 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ (๐บ supp โ
) โ ๐) |
74 | 13, 67, 68, 69, 70, 72, 73, 1 | cantnfp1lem1 9622 |
. . 3
โข ((๐ โง ๐ โ โ
) โ ๐น โ ๐) |
75 | | onelon 6346 |
. . . . . . 7
โข ((๐ด โ On โง ๐ โ ๐ด) โ ๐ โ On) |
76 | 14, 71, 75 | syl2anc 585 |
. . . . . 6
โข (๐ โ ๐ โ On) |
77 | | on0eln0 6377 |
. . . . . 6
โข (๐ โ On โ (โ
โ ๐ โ ๐ โ โ
)) |
78 | 76, 77 | syl 17 |
. . . . 5
โข (๐ โ (โ
โ ๐ โ ๐ โ โ
)) |
79 | 78 | biimpar 479 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ โ
โ ๐) |
80 | | eqid 2733 |
. . . 4
โข OrdIso( E
, (๐น supp โ
)) =
OrdIso( E , (๐น supp
โ
)) |
81 | | eqid 2733 |
. . . 4
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
) =
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
) |
82 | | eqid 2733 |
. . . 4
โข OrdIso( E
, (๐บ supp โ
)) =
OrdIso( E , (๐บ supp
โ
)) |
83 | | eqid 2733 |
. . . 4
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , (๐บ supp โ
))โ๐)) ยทo (๐บโ(OrdIso( E , (๐บ supp โ
))โ๐))) +o ๐ง)), โ
) =
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , (๐บ supp โ
))โ๐)) ยทo (๐บโ(OrdIso( E , (๐บ supp โ
))โ๐))) +o ๐ง)), โ
) |
84 | 13, 67, 68, 69, 70, 72, 73, 1, 79, 80, 81, 82, 83 | cantnfp1lem3 9624 |
. . 3
โข ((๐ โง ๐ โ โ
) โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
85 | 74, 84 | jca 513 |
. 2
โข ((๐ โง ๐ โ โ
) โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |
86 | 66, 85 | pm2.61dane 3029 |
1
โข (๐ โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |