Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . . . 5
โข ๐ = dom (๐ด CNF ๐ต) |
2 | | cantnfs.a |
. . . . 5
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . . . 5
โข (๐ โ ๐ต โ On) |
4 | | cantnf.g |
. . . . 5
โข (๐ โ ๐บ โ ๐) |
5 | | oemapval.t |
. . . . . . . . . . . . . 14
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} |
6 | | cantnf.c |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ถ โ (๐ด โo ๐ต)) |
7 | | cantnf.s |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ถ โ ran (๐ด CNF ๐ต)) |
8 | | cantnf.e |
. . . . . . . . . . . . . 14
โข (๐ โ โ
โ ๐ถ) |
9 | 1, 2, 3, 5, 6, 7, 8 | cantnflem2 9633 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โ (On โ 2o) โง
๐ถ โ (On โ
1o))) |
10 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข ๐ = ๐ |
11 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข ๐ = ๐ |
12 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข ๐ = ๐ |
13 | 10, 11, 12 | 3pm3.2i 1340 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โง ๐ = ๐ โง ๐ = ๐) |
14 | | cantnf.x |
. . . . . . . . . . . . . . 15
โข ๐ = โช
โฉ {๐ โ On โฃ ๐ถ โ (๐ด โo ๐)} |
15 | | cantnf.p |
. . . . . . . . . . . . . . 15
โข ๐ = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
16 | | cantnf.y |
. . . . . . . . . . . . . . 15
โข ๐ = (1st โ๐) |
17 | | cantnf.z |
. . . . . . . . . . . . . . 15
โข ๐ = (2nd โ๐) |
18 | 14, 15, 16, 17 | oeeui 8554 |
. . . . . . . . . . . . . 14
โข ((๐ด โ (On โ
2o) โง ๐ถ
โ (On โ 1o)) โ (((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ) โ (๐ = ๐ โง ๐ = ๐ โง ๐ = ๐))) |
19 | 13, 18 | mpbiri 258 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ถ
โ (On โ 1o)) โ ((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
20 | 9, 19 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
21 | 20 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐))) |
22 | 21 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ ๐ โ On) |
23 | | oecl 8488 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ โ On) โ (๐ด โo ๐) โ On) |
24 | 2, 22, 23 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ด โo ๐) โ On) |
25 | 21 | simp2d 1144 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐ด โ 1o)) |
26 | 25 | eldifad 3927 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ด) |
27 | | onelon 6347 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ โ ๐ด) โ ๐ โ On) |
28 | 2, 26, 27 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ๐ โ On) |
29 | | dif1o 8451 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด โ 1o) โ (๐ โ ๐ด โง ๐ โ โ
)) |
30 | 29 | simprbi 498 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ 1o) โ ๐ โ โ
) |
31 | 25, 30 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ
) |
32 | | on0eln0 6378 |
. . . . . . . . . . 11
โข (๐ โ On โ (โ
โ ๐ โ ๐ โ โ
)) |
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โ
โ ๐ โ ๐ โ โ
)) |
34 | 31, 33 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ โ
โ ๐) |
35 | | omword1 8525 |
. . . . . . . . 9
โข ((((๐ด โo ๐) โ On โง ๐ โ On) โง โ
โ
๐) โ (๐ด โo ๐) โ ((๐ด โo ๐) ยทo ๐)) |
36 | 24, 28, 34, 35 | syl21anc 837 |
. . . . . . . 8
โข (๐ โ (๐ด โo ๐) โ ((๐ด โo ๐) ยทo ๐)) |
37 | | omcl 8487 |
. . . . . . . . . . 11
โข (((๐ด โo ๐) โ On โง ๐ โ On) โ ((๐ด โo ๐) ยทo ๐) โ On) |
38 | 24, 28, 37 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ด โo ๐) ยทo ๐) โ On) |
39 | 21 | simp3d 1145 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐ด โo ๐)) |
40 | | onelon 6347 |
. . . . . . . . . . 11
โข (((๐ด โo ๐) โ On โง ๐ โ (๐ด โo ๐)) โ ๐ โ On) |
41 | 24, 39, 40 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ๐ โ On) |
42 | | oaword1 8504 |
. . . . . . . . . 10
โข ((((๐ด โo ๐) ยทo ๐) โ On โง ๐ โ On) โ ((๐ด โo ๐) ยทo ๐) โ (((๐ด โo ๐) ยทo ๐) +o ๐)) |
43 | 38, 41, 42 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((๐ด โo ๐) ยทo ๐) โ (((๐ด โo ๐) ยทo ๐) +o ๐)) |
44 | 20 | simprd 497 |
. . . . . . . . 9
โข (๐ โ (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ) |
45 | 43, 44 | sseqtrd 3989 |
. . . . . . . 8
โข (๐ โ ((๐ด โo ๐) ยทo ๐) โ ๐ถ) |
46 | 36, 45 | sstrd 3959 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐) โ ๐ถ) |
47 | | oecl 8488 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
48 | 2, 3, 47 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (๐ด โo ๐ต) โ On) |
49 | | ontr2 6369 |
. . . . . . . 8
โข (((๐ด โo ๐) โ On โง (๐ด โo ๐ต) โ On) โ (((๐ด โo ๐) โ ๐ถ โง ๐ถ โ (๐ด โo ๐ต)) โ (๐ด โo ๐) โ (๐ด โo ๐ต))) |
50 | 24, 48, 49 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (((๐ด โo ๐) โ ๐ถ โง ๐ถ โ (๐ด โo ๐ต)) โ (๐ด โo ๐) โ (๐ด โo ๐ต))) |
51 | 46, 6, 50 | mp2and 698 |
. . . . . 6
โข (๐ โ (๐ด โo ๐) โ (๐ด โo ๐ต)) |
52 | 9 | simpld 496 |
. . . . . . 7
โข (๐ โ ๐ด โ (On โ
2o)) |
53 | | oeord 8540 |
. . . . . . 7
โข ((๐ โ On โง ๐ต โ On โง ๐ด โ (On โ
2o)) โ (๐
โ ๐ต โ (๐ด โo ๐) โ (๐ด โo ๐ต))) |
54 | 22, 3, 52, 53 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (๐ โ ๐ต โ (๐ด โo ๐) โ (๐ด โo ๐ต))) |
55 | 51, 54 | mpbird 257 |
. . . . 5
โข (๐ โ ๐ โ ๐ต) |
56 | 2 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ด โ On) |
57 | 3 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ต โ On) |
58 | | suppssdm 8113 |
. . . . . . . . . . . . . . 15
โข (๐บ supp โ
) โ dom ๐บ |
59 | 1, 2, 3 | cantnfs 9609 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บ โ ๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
))) |
60 | 4, 59 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
)) |
61 | 60 | simpld 496 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐บ:๐ตโถ๐ด) |
62 | 58, 61 | fssdm 6693 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐บ supp โ
) โ ๐ต) |
63 | 62 | sselda 3949 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ฅ โ ๐ต) |
64 | | onelon 6347 |
. . . . . . . . . . . . 13
โข ((๐ต โ On โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
65 | 57, 63, 64 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ฅ โ On) |
66 | | oecl 8488 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ฅ โ On) โ (๐ด โo ๐ฅ) โ On) |
67 | 56, 65, 66 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ด โo ๐ฅ) โ On) |
68 | 61 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐บ:๐ตโถ๐ด) |
69 | 68, 63 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐บโ๐ฅ) โ ๐ด) |
70 | | onelon 6347 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง (๐บโ๐ฅ) โ ๐ด) โ (๐บโ๐ฅ) โ On) |
71 | 56, 69, 70 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐บโ๐ฅ) โ On) |
72 | 61 | ffnd 6674 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐บ Fn ๐ต) |
73 | 8 | elexd 3468 |
. . . . . . . . . . . . . 14
โข (๐ โ โ
โ
V) |
74 | | elsuppfn 8107 |
. . . . . . . . . . . . . 14
โข ((๐บ Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(๐ฅ โ (๐บ supp โ
) โ (๐ฅ โ ๐ต โง (๐บโ๐ฅ) โ โ
))) |
75 | 72, 3, 73, 74 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ (๐บ supp โ
) โ (๐ฅ โ ๐ต โง (๐บโ๐ฅ) โ โ
))) |
76 | 75 | simplbda 501 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐บโ๐ฅ) โ โ
) |
77 | | on0eln0 6378 |
. . . . . . . . . . . . 13
โข ((๐บโ๐ฅ) โ On โ (โ
โ (๐บโ๐ฅ) โ (๐บโ๐ฅ) โ โ
)) |
78 | 71, 77 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (โ
โ
(๐บโ๐ฅ) โ (๐บโ๐ฅ) โ โ
)) |
79 | 76, 78 | mpbird 257 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ โ
โ (๐บโ๐ฅ)) |
80 | | omword1 8525 |
. . . . . . . . . . 11
โข ((((๐ด โo ๐ฅ) โ On โง (๐บโ๐ฅ) โ On) โง โ
โ (๐บโ๐ฅ)) โ (๐ด โo ๐ฅ) โ ((๐ด โo ๐ฅ) ยทo (๐บโ๐ฅ))) |
81 | 67, 71, 79, 80 | syl21anc 837 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ด โo ๐ฅ) โ ((๐ด โo ๐ฅ) ยทo (๐บโ๐ฅ))) |
82 | | eqid 2737 |
. . . . . . . . . . . 12
โข OrdIso( E
, (๐บ supp โ
)) =
OrdIso( E , (๐บ supp
โ
)) |
83 | 4 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐บ โ ๐) |
84 | | eqid 2737 |
. . . . . . . . . . . 12
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , (๐บ supp โ
))โ๐)) ยทo (๐บโ(OrdIso( E , (๐บ supp โ
))โ๐))) +o ๐ง)), โ
) =
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , (๐บ supp โ
))โ๐)) ยทo (๐บโ(OrdIso( E , (๐บ supp โ
))โ๐))) +o ๐ง)), โ
) |
85 | 1, 56, 57, 82, 83, 84, 63 | cantnfle 9614 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ((๐ด โo ๐ฅ) ยทo (๐บโ๐ฅ)) โ ((๐ด CNF ๐ต)โ๐บ)) |
86 | | cantnf.v |
. . . . . . . . . . . 12
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) = ๐) |
87 | 86 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ((๐ด CNF ๐ต)โ๐บ) = ๐) |
88 | 85, 87 | sseqtrd 3989 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ((๐ด โo ๐ฅ) ยทo (๐บโ๐ฅ)) โ ๐) |
89 | 81, 88 | sstrd 3959 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ด โo ๐ฅ) โ ๐) |
90 | 39 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ โ (๐ด โo ๐)) |
91 | 24 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ด โo ๐) โ On) |
92 | | ontr2 6369 |
. . . . . . . . . 10
โข (((๐ด โo ๐ฅ) โ On โง (๐ด โo ๐) โ On) โ (((๐ด โo ๐ฅ) โ ๐ โง ๐ โ (๐ด โo ๐)) โ (๐ด โo ๐ฅ) โ (๐ด โo ๐))) |
93 | 67, 91, 92 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (((๐ด โo ๐ฅ) โ ๐ โง ๐ โ (๐ด โo ๐)) โ (๐ด โo ๐ฅ) โ (๐ด โo ๐))) |
94 | 89, 90, 93 | mp2and 698 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ด โo ๐ฅ) โ (๐ด โo ๐)) |
95 | 22 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ โ On) |
96 | 52 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ด โ (On โ
2o)) |
97 | | oeord 8540 |
. . . . . . . . 9
โข ((๐ฅ โ On โง ๐ โ On โง ๐ด โ (On โ
2o)) โ (๐ฅ
โ ๐ โ (๐ด โo ๐ฅ) โ (๐ด โo ๐))) |
98 | 65, 95, 96, 97 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ (๐ฅ โ ๐ โ (๐ด โo ๐ฅ) โ (๐ด โo ๐))) |
99 | 94, 98 | mpbird 257 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐บ supp โ
)) โ ๐ฅ โ ๐) |
100 | 99 | ex 414 |
. . . . . 6
โข (๐ โ (๐ฅ โ (๐บ supp โ
) โ ๐ฅ โ ๐)) |
101 | 100 | ssrdv 3955 |
. . . . 5
โข (๐ โ (๐บ supp โ
) โ ๐) |
102 | | cantnf.f |
. . . . 5
โข ๐น = (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐บโ๐ก))) |
103 | 1, 2, 3, 4, 55, 26, 101, 102 | cantnfp1 9624 |
. . . 4
โข (๐ โ (๐น โ ๐ โง ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)))) |
104 | 103 | simprd 497 |
. . 3
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ))) |
105 | 86 | oveq2d 7378 |
. . 3
โข (๐ โ (((๐ด โo ๐) ยทo ๐) +o ((๐ด CNF ๐ต)โ๐บ)) = (((๐ด โo ๐) ยทo ๐) +o ๐)) |
106 | 104, 105,
44 | 3eqtrd 2781 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = ๐ถ) |
107 | 1, 2, 3 | cantnff 9617 |
. . . 4
โข (๐ โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
108 | 107 | ffnd 6674 |
. . 3
โข (๐ โ (๐ด CNF ๐ต) Fn ๐) |
109 | 103 | simpld 496 |
. . 3
โข (๐ โ ๐น โ ๐) |
110 | | fnfvelrn 7036 |
. . 3
โข (((๐ด CNF ๐ต) Fn ๐ โง ๐น โ ๐) โ ((๐ด CNF ๐ต)โ๐น) โ ran (๐ด CNF ๐ต)) |
111 | 108, 109,
110 | syl2anc 585 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) โ ran (๐ด CNF ๐ต)) |
112 | 106, 111 | eqeltrrd 2839 |
1
โข (๐ โ ๐ถ โ ran (๐ด CNF ๐ต)) |