Step | Hyp | Ref
| Expression |
1 | | cantnf.s |
. . . 4
โข (๐ โ ๐ถ โ ran (๐ด CNF ๐ต)) |
2 | | cantnfs.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.s |
. . . . . . . . . . . . 13
โข ๐ = dom (๐ด CNF ๐ต) |
4 | | cantnfs.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ On) |
5 | | oemapval.t |
. . . . . . . . . . . . 13
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} |
6 | | cantnf.c |
. . . . . . . . . . . . 13
โข (๐ โ ๐ถ โ (๐ด โo ๐ต)) |
7 | | cantnf.e |
. . . . . . . . . . . . 13
โข (๐ โ โ
โ ๐ถ) |
8 | 3, 2, 4, 5, 6, 1, 7 | cantnflem2 9634 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด โ (On โ 2o) โง
๐ถ โ (On โ
1o))) |
9 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข ๐ = ๐ |
10 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข ๐ = ๐ |
11 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข ๐ = ๐ |
12 | 9, 10, 11 | 3pm3.2i 1340 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โง ๐ = ๐ โง ๐ = ๐) |
13 | | cantnf.x |
. . . . . . . . . . . . . 14
โข ๐ = โช
โฉ {๐ โ On โฃ ๐ถ โ (๐ด โo ๐)} |
14 | | cantnf.p |
. . . . . . . . . . . . . 14
โข ๐ = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
15 | | cantnf.y |
. . . . . . . . . . . . . 14
โข ๐ = (1st โ๐) |
16 | | cantnf.z |
. . . . . . . . . . . . . 14
โข ๐ = (2nd โ๐) |
17 | 13, 14, 15, 16 | oeeui 8553 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ถ
โ (On โ 1o)) โ (((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ) โ (๐ = ๐ โง ๐ = ๐ โง ๐ = ๐))) |
18 | 12, 17 | mpbiri 258 |
. . . . . . . . . . . 12
โข ((๐ด โ (On โ
2o) โง ๐ถ
โ (On โ 1o)) โ ((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
19 | 8, 18 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐)) โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ)) |
20 | 19 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ (๐ โ On โง ๐ โ (๐ด โ 1o) โง ๐ โ (๐ด โo ๐))) |
21 | 20 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ โ On) |
22 | | oecl 8487 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ โ On) โ (๐ด โo ๐) โ On) |
23 | 2, 21, 22 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (๐ด โo ๐) โ On) |
24 | 20 | simp2d 1144 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ด โ 1o)) |
25 | 24 | eldifad 3926 |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐ด) |
26 | | onelon 6346 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ โ ๐ด) โ ๐ โ On) |
27 | 2, 25, 26 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ๐ โ On) |
28 | | omcl 8486 |
. . . . . . . 8
โข (((๐ด โo ๐) โ On โง ๐ โ On) โ ((๐ด โo ๐) ยทo ๐) โ On) |
29 | 23, 27, 28 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ด โo ๐) ยทo ๐) โ On) |
30 | 20 | simp3d 1145 |
. . . . . . . 8
โข (๐ โ ๐ โ (๐ด โo ๐)) |
31 | | onelon 6346 |
. . . . . . . 8
โข (((๐ด โo ๐) โ On โง ๐ โ (๐ด โo ๐)) โ ๐ โ On) |
32 | 23, 30, 31 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ๐ โ On) |
33 | | oaword1 8503 |
. . . . . . 7
โข ((((๐ด โo ๐) ยทo ๐) โ On โง ๐ โ On) โ ((๐ด โo ๐) ยทo ๐) โ (((๐ด โo ๐) ยทo ๐) +o ๐)) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ด โo ๐) ยทo ๐) โ (((๐ด โo ๐) ยทo ๐) +o ๐)) |
35 | | dif1o 8450 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ 1o) โ (๐ โ ๐ด โง ๐ โ โ
)) |
36 | 35 | simprbi 498 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ 1o) โ ๐ โ โ
) |
37 | 24, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ
) |
38 | | on0eln0 6377 |
. . . . . . . . . 10
โข (๐ โ On โ (โ
โ ๐ โ ๐ โ โ
)) |
39 | 27, 38 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โ
โ ๐ โ ๐ โ โ
)) |
40 | 37, 39 | mpbird 257 |
. . . . . . . 8
โข (๐ โ โ
โ ๐) |
41 | | omword1 8524 |
. . . . . . . 8
โข ((((๐ด โo ๐) โ On โง ๐ โ On) โง โ
โ
๐) โ (๐ด โo ๐) โ ((๐ด โo ๐) ยทo ๐)) |
42 | 23, 27, 40, 41 | syl21anc 837 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐) โ ((๐ด โo ๐) ยทo ๐)) |
43 | 42, 30 | sseldd 3949 |
. . . . . 6
โข (๐ โ ๐ โ ((๐ด โo ๐) ยทo ๐)) |
44 | 34, 43 | sseldd 3949 |
. . . . 5
โข (๐ โ ๐ โ (((๐ด โo ๐) ยทo ๐) +o ๐)) |
45 | 19 | simprd 497 |
. . . . 5
โข (๐ โ (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ถ) |
46 | 44, 45 | eleqtrd 2836 |
. . . 4
โข (๐ โ ๐ โ ๐ถ) |
47 | 1, 46 | sseldd 3949 |
. . 3
โข (๐ โ ๐ โ ran (๐ด CNF ๐ต)) |
48 | 3, 2, 4 | cantnff 9618 |
. . . 4
โข (๐ โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
49 | | ffn 6672 |
. . . 4
โข ((๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต) โ (๐ด CNF ๐ต) Fn ๐) |
50 | | fvelrnb 6907 |
. . . 4
โข ((๐ด CNF ๐ต) Fn ๐ โ (๐ โ ran (๐ด CNF ๐ต) โ โ๐ โ ๐ ((๐ด CNF ๐ต)โ๐) = ๐)) |
51 | 48, 49, 50 | 3syl 18 |
. . 3
โข (๐ โ (๐ โ ran (๐ด CNF ๐ต) โ โ๐ โ ๐ ((๐ด CNF ๐ต)โ๐) = ๐)) |
52 | 47, 51 | mpbid 231 |
. 2
โข (๐ โ โ๐ โ ๐ ((๐ด CNF ๐ต)โ๐) = ๐) |
53 | 2 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ด โ On) |
54 | 4 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ต โ On) |
55 | 6 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ถ โ (๐ด โo ๐ต)) |
56 | 1 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ถ โ ran (๐ด CNF ๐ต)) |
57 | 7 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ โ
โ ๐ถ) |
58 | | simprl 770 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ โ ๐) |
59 | | simprr 772 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ((๐ด CNF ๐ต)โ๐) = ๐) |
60 | | eqid 2733 |
. . 3
โข (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐โ๐ก))) = (๐ก โ ๐ต โฆ if(๐ก = ๐, ๐, (๐โ๐ก))) |
61 | 3, 53, 54, 5, 55, 56, 57, 13, 14, 15, 16, 58, 59, 60 | cantnflem3 9635 |
. 2
โข ((๐ โง (๐ โ ๐ โง ((๐ด CNF ๐ต)โ๐) = ๐)) โ ๐ถ โ ran (๐ด CNF ๐ต)) |
62 | 52, 61 | rexlimddv 3155 |
1
โข (๐ โ ๐ถ โ ran (๐ด CNF ๐ต)) |