Step | Hyp | Ref
| Expression |
1 | | cantnfp1.f |
. . . . . 6
โข ๐น = (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) |
2 | | cantnfs.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ On) |
3 | | cantnfp1.x |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐ต) |
4 | | onelon 6389 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ โ ๐ต) โ ๐ โ On) |
5 | 2, 3, 4 | syl2anc 584 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ On) |
6 | | eloni 6374 |
. . . . . . . . . . . 12
โข (๐ โ On โ Ord ๐) |
7 | | ordirr 6382 |
. . . . . . . . . . . 12
โข (Ord
๐ โ ยฌ ๐ โ ๐) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ ยฌ ๐ โ ๐) |
9 | | fvex 6904 |
. . . . . . . . . . . . . 14
โข (๐บโ๐) โ V |
10 | | dif1o 8499 |
. . . . . . . . . . . . . 14
โข ((๐บโ๐) โ (V โ 1o) โ
((๐บโ๐) โ V โง (๐บโ๐) โ โ
)) |
11 | 9, 10 | mpbiran 707 |
. . . . . . . . . . . . 13
โข ((๐บโ๐) โ (V โ 1o) โ
(๐บโ๐) โ โ
) |
12 | | cantnfp1.g |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐บ โ ๐) |
13 | | cantnfs.s |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ = dom (๐ด CNF ๐ต) |
14 | | cantnfs.a |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ด โ On) |
15 | 13, 14, 2 | cantnfs 9660 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐บ โ ๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
))) |
16 | 12, 15 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
)) |
17 | 16 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บ:๐ตโถ๐ด) |
18 | 17 | ffnd 6718 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐บ Fn ๐ต) |
19 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . 18
โข โ
โ V |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ
โ
V) |
21 | | elsuppfn 8155 |
. . . . . . . . . . . . . . . . 17
โข ((๐บ Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
22 | 18, 2, 20, 21 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ โ
))) |
23 | 11 | bicomi 223 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บโ๐) โ โ
โ (๐บโ๐) โ (V โ
1o)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐บโ๐) โ โ
โ (๐บโ๐) โ (V โ
1o))) |
25 | 24 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
26 | 22, 25 | bitrd 278 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ (๐บ supp โ
) โ (๐ โ ๐ต โง (๐บโ๐) โ (V โ
1o)))) |
27 | | cantnfp1.s |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐บ supp โ
) โ ๐) |
28 | 27 | sseld 3981 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ (๐บ supp โ
) โ ๐ โ ๐)) |
29 | 26, 28 | sylbird 259 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ โ ๐ต โง (๐บโ๐) โ (V โ 1o)) โ
๐ โ ๐)) |
30 | 3, 29 | mpand 693 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐บโ๐) โ (V โ 1o) โ
๐ โ ๐)) |
31 | 11, 30 | biimtrrid 242 |
. . . . . . . . . . . 12
โข (๐ โ ((๐บโ๐) โ โ
โ ๐ โ ๐)) |
32 | 31 | necon1bd 2958 |
. . . . . . . . . . 11
โข (๐ โ (ยฌ ๐ โ ๐ โ (๐บโ๐) = โ
)) |
33 | 8, 32 | mpd 15 |
. . . . . . . . . 10
โข (๐ โ (๐บโ๐) = โ
) |
34 | 33 | ad3antrrr 728 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ (๐บโ๐) = โ
) |
35 | | simpr 485 |
. . . . . . . . . 10
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ก = ๐) |
36 | 35 | fveq2d 6895 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ (๐บโ๐ก) = (๐บโ๐)) |
37 | | simpllr 774 |
. . . . . . . . 9
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ = โ
) |
38 | 34, 36, 37 | 3eqtr4rd 2783 |
. . . . . . . 8
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ๐ก = ๐) โ ๐ = (๐บโ๐ก)) |
39 | | eqidd 2733 |
. . . . . . . 8
โข ((((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โง ยฌ ๐ก = ๐) โ (๐บโ๐ก) = (๐บโ๐ก)) |
40 | 38, 39 | ifeqda 4564 |
. . . . . . 7
โข (((๐ โง ๐ = โ
) โง ๐ก โ ๐ต) โ if(๐ก = ๐, ๐, (๐บโ๐ก)) = (๐บโ๐ก)) |
41 | 40 | mpteq2dva 5248 |
. . . . . 6
โข ((๐ โง ๐ = โ
) โ (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
42 | 1, 41 | eqtrid 2784 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ๐น = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
43 | 17 | feqmptd 6960 |
. . . . . 6
โข (๐ โ ๐บ = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
44 | 43 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ๐บ = (๐ก โ ๐ต โฆ (๐บโ๐ก))) |
45 | 42, 44 | eqtr4d 2775 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ๐น = ๐บ) |
46 | 12 | adantr 481 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ๐บ โ ๐) |
47 | 45, 46 | eqeltrd 2833 |
. . 3
โข ((๐ โง ๐ = โ
) โ ๐น โ ๐) |
48 | | oecl 8536 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
49 | 14, 2, 48 | syl2anc 584 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐ต) โ On) |
50 | 13, 14, 2 | cantnff 9668 |
. . . . . . . 8
โข (๐ โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
51 | 50, 12 | ffvelcdmd 7087 |
. . . . . . 7
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) โ (๐ด โo ๐ต)) |
52 | | onelon 6389 |
. . . . . . 7
โข (((๐ด โo ๐ต) โ On โง ((๐ด CNF ๐ต)โ๐บ) โ (๐ด โo ๐ต)) โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
53 | 49, 51, 52 | syl2anc 584 |
. . . . . 6
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
54 | 53 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐บ) โ On) |
55 | | oa0r 8537 |
. . . . 5
โข (((๐ด CNF ๐ต)โ๐บ) โ On โ (โ
+o
((๐ด CNF ๐ต)โ๐บ)) = ((๐ด CNF ๐ต)โ๐บ)) |
56 | 54, 55 | syl 17 |
. . . 4
โข ((๐ โง ๐ = โ
) โ (โ
+o
((๐ด CNF ๐ต)โ๐บ)) = ((๐ด CNF ๐ต)โ๐บ)) |
57 | | oveq2 7416 |
. . . . . 6
โข (๐ = โ
โ ((๐ด โo ๐) ยทo ๐) = ((๐ด โo ๐) ยทo
โ
)) |
58 | | oecl 8536 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ โ On) โ (๐ด โo ๐) โ On) |
59 | 14, 5, 58 | syl2anc 584 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐) โ On) |
60 | | om0 8516 |
. . . . . . 7
โข ((๐ด โo ๐) โ On โ ((๐ด โo ๐) ยทo โ
)
= โ
) |
61 | 59, 60 | syl 17 |
. . . . . 6
โข (๐ โ ((๐ด โo ๐) ยทo โ
) =
โ
) |
62 | 57, 61 | sylan9eqr 2794 |
. . . . 5
โข ((๐ โง ๐ = โ
) โ ((๐ด โo ๐) ยทo ๐) = โ
) |
63 | 62 | oveq1d 7423 |
. . . 4
โข ((๐ โง ๐ = โ
) โ (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)) = (โ
+o ((๐ด CNF ๐ต)โ๐บ))) |
64 | 45 | fveq2d 6895 |
. . . 4
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐น) = ((๐ด CNF ๐ต)โ๐บ)) |
65 | 56, 63, 64 | 3eqtr4rd 2783 |
. . 3
โข ((๐ โง ๐ = โ
) โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
66 | 47, 65 | jca 512 |
. 2
โข ((๐ โง ๐ = โ
) โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |
67 | 14 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ด โ On) |
68 | 2 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ต โ On) |
69 | 12 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐บ โ ๐) |
70 | 3 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ โ ๐ต) |
71 | | cantnfp1.y |
. . . . 5
โข (๐ โ ๐ โ ๐ด) |
72 | 71 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ ๐ โ ๐ด) |
73 | 27 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ (๐บ supp โ
) โ ๐) |
74 | 13, 67, 68, 69, 70, 72, 73, 1 | cantnfp1lem1 9672 |
. . 3
โข ((๐ โง ๐ โ โ
) โ ๐น โ ๐) |
75 | | onelon 6389 |
. . . . . . 7
โข ((๐ด โ On โง ๐ โ ๐ด) โ ๐ โ On) |
76 | 14, 71, 75 | syl2anc 584 |
. . . . . 6
โข (๐ โ ๐ โ On) |
77 | | on0eln0 6420 |
. . . . . 6
โข (๐ โ On โ (โ
โ ๐ โ ๐ โ โ
)) |
78 | 76, 77 | syl 17 |
. . . . 5
โข (๐ โ (โ
โ ๐ โ ๐ โ โ
)) |
79 | 78 | biimpar 478 |
. . . 4
โข ((๐ โง ๐ โ โ
) โ โ
โ ๐) |
80 | | eqid 2732 |
. . . 4
โข OrdIso( E
, (๐น supp โ
)) =
OrdIso( E , (๐น supp
โ
)) |
81 | | eqid 2732 |
. . . 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 2732 |
. . . 4
โข OrdIso( E
, (๐บ supp โ
)) =
OrdIso( E , (๐บ supp
โ
)) |
83 | | eqid 2732 |
. . . 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 9674 |
. . 3
โข ((๐ โง ๐ โ โ
) โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
85 | 74, 84 | jca 512 |
. 2
โข ((๐ โง ๐ โ โ
) โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |
86 | 66, 85 | pm2.61dane 3029 |
1
โข (๐ โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |