Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
โข ๐ = dom (๐ด CNF ๐ต) |
2 | | cantnfs.a |
. . 3
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . 3
โข (๐ โ ๐ต โ On) |
4 | | oemapval.t |
. . 3
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} |
5 | 1, 2, 3, 4 | oemapso 9626 |
. 2
โข (๐ โ ๐ Or ๐) |
6 | | oecl 8487 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
7 | 2, 3, 6 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ด โo ๐ต) โ On) |
8 | | eloni 6331 |
. . . 4
โข ((๐ด โo ๐ต) โ On โ Ord (๐ด โo ๐ต)) |
9 | 7, 8 | syl 17 |
. . 3
โข (๐ โ Ord (๐ด โo ๐ต)) |
10 | | ordwe 6334 |
. . 3
โข (Ord
(๐ด โo ๐ต) โ E We (๐ด โo ๐ต)) |
11 | | weso 5628 |
. . 3
โข ( E We
(๐ด โo ๐ต) โ E Or (๐ด โo ๐ต)) |
12 | | sopo 5568 |
. . 3
โข ( E Or
(๐ด โo ๐ต) โ E Po (๐ด โo ๐ต)) |
13 | 9, 10, 11, 12 | 4syl 19 |
. 2
โข (๐ โ E Po (๐ด โo ๐ต)) |
14 | 1, 2, 3 | cantnff 9618 |
. . 3
โข (๐ โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
15 | 14 | frnd 6680 |
. . . 4
โข (๐ โ ran (๐ด CNF ๐ต) โ (๐ด โo ๐ต)) |
16 | | onss 7723 |
. . . . . . . 8
โข ((๐ด โo ๐ต) โ On โ (๐ด โo ๐ต) โ On) |
17 | 7, 16 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ด โo ๐ต) โ On) |
18 | 17 | sseld 3947 |
. . . . . 6
โข (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ On)) |
19 | | eleq1w 2817 |
. . . . . . . . . 10
โข (๐ก = ๐ฆ โ (๐ก โ (๐ด โo ๐ต) โ ๐ฆ โ (๐ด โo ๐ต))) |
20 | | eleq1w 2817 |
. . . . . . . . . 10
โข (๐ก = ๐ฆ โ (๐ก โ ran (๐ด CNF ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))) |
21 | 19, 20 | imbi12d 345 |
. . . . . . . . 9
โข (๐ก = ๐ฆ โ ((๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต)) โ (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)))) |
22 | 21 | imbi2d 341 |
. . . . . . . 8
โข (๐ก = ๐ฆ โ ((๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ โ (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))))) |
23 | | r19.21v 3173 |
. . . . . . . . 9
โข
(โ๐ฆ โ
๐ก (๐ โ (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))) โ (๐ โ โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)))) |
24 | | ordelss 6337 |
. . . . . . . . . . . . . . . . . . 19
โข ((Ord
(๐ด โo ๐ต) โง ๐ก โ (๐ด โo ๐ต)) โ ๐ก โ (๐ด โo ๐ต)) |
25 | 9, 24 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ (๐ด โo ๐ต)) โ ๐ก โ (๐ด โo ๐ต)) |
26 | 25 | sselda 3948 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ก โ (๐ด โo ๐ต)) โง ๐ฆ โ ๐ก) โ ๐ฆ โ (๐ด โo ๐ต)) |
27 | | pm5.5 362 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ (๐ด โo ๐ต) โ ((๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ ๐ฆ โ ran (๐ด CNF ๐ต))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ก โ (๐ด โo ๐ต)) โง ๐ฆ โ ๐ก) โ ((๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ ๐ฆ โ ran (๐ด CNF ๐ต))) |
29 | 28 | ralbidva 3169 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ก โ (๐ด โo ๐ต)) โ (โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ โ๐ฆ โ ๐ก ๐ฆ โ ran (๐ด CNF ๐ต))) |
30 | | dfss3 3936 |
. . . . . . . . . . . . . . 15
โข (๐ก โ ran (๐ด CNF ๐ต) โ โ๐ฆ โ ๐ก ๐ฆ โ ran (๐ด CNF ๐ต)) |
31 | 29, 30 | bitr4di 289 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ก โ (๐ด โo ๐ต)) โ (โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ ๐ก โ ran (๐ด CNF ๐ต))) |
32 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
โข (๐ก = โ
โ (๐ก โ ran (๐ด CNF ๐ต) โ โ
โ ran (๐ด CNF ๐ต))) |
33 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ๐ด โ On) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ ๐ด โ On) |
35 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ๐ต โ On) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ ๐ต โ On) |
37 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ ๐ก โ (๐ด โo ๐ต)) |
38 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ ๐ก โ ran (๐ด CNF ๐ต)) |
39 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ด โo ๐ต) โ On) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ๐ก โ (๐ด โo ๐ต)) |
41 | | onelon 6346 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โo ๐ต) โ On โง ๐ก โ (๐ด โo ๐ต)) โ ๐ก โ On) |
42 | 39, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ๐ก โ On) |
43 | | on0eln0 6377 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ก โ On โ (โ
โ ๐ก โ ๐ก โ โ
)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (โ
โ ๐ก โ ๐ก โ โ
)) |
45 | 44 | biimpar 479 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ โ
โ ๐ก) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)} = โช โฉ {๐
โ On โฃ ๐ก โ
(๐ด โo ๐)} |
47 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก)) = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก)) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก))) = (1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก))) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก))) = (2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ก โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ก))) |
50 | 1, 34, 36, 4, 37, 38, 45, 46, 47, 48, 49 | cantnflem4 9636 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ก โ โ
) โ ๐ก โ ran (๐ด CNF ๐ต)) |
51 | | fczsupp0 8128 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต ร {โ
}) supp
โ
) = โ
|
52 | 51 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . 20
โข โ
=
((๐ต ร {โ
}) supp
โ
) |
53 | | oieq2 9457 |
. . . . . . . . . . . . . . . . . . . 20
โข (โ
= ((๐ต ร {โ
})
supp โ
) โ OrdIso( E , โ
) = OrdIso( E , ((๐ต ร {โ
}) supp
โ
))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข OrdIso( E
, โ
) = OrdIso( E , ((๐ต ร {โ
}) supp
โ
)) |
55 | | ne0i 4298 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ก โ (๐ด โo ๐ต) โ (๐ด โo ๐ต) โ โ
) |
56 | 55 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ด โo ๐ต) โ โ
) |
57 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ด = โ
โ (๐ด โo ๐ต) = (โ
โo
๐ต)) |
58 | 57 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ด = โ
โ ((๐ด โo ๐ต) โ โ
โ (โ
โo ๐ต) โ
โ
)) |
59 | 56, 58 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ด = โ
โ (โ
โo ๐ต) โ
โ
)) |
60 | 59 | necon2d 2963 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ((โ
โo
๐ต) = โ
โ ๐ด โ โ
)) |
61 | | on0eln0 6377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ต โ On โ (โ
โ ๐ต โ ๐ต โ โ
)) |
62 | | oe0m1 8471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ต โ On โ (โ
โ ๐ต โ (โ
โo ๐ต) =
โ
)) |
63 | 61, 62 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ต โ On โ (๐ต โ โ
โ (โ
โo ๐ต) =
โ
)) |
64 | 35, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ต โ โ
โ (โ
โo ๐ต) =
โ
)) |
65 | | on0eln0 6377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ด โ On โ (โ
โ ๐ด โ ๐ด โ โ
)) |
66 | 33, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (โ
โ ๐ด โ ๐ด โ โ
)) |
67 | 60, 64, 66 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ต โ โ
โ โ
โ ๐ด)) |
68 | | ne0i 4298 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ ๐ต โ ๐ต โ โ
) |
69 | 67, 68 | impel 507 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โง ๐ฆ โ ๐ต) โ โ
โ ๐ด) |
70 | | fconstmpt 5698 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ต ร {โ
}) = (๐ฆ โ ๐ต โฆ โ
) |
71 | 69, 70 | fmptd 7066 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ต ร {โ
}):๐ตโถ๐ด) |
72 | | 0ex 5268 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข โ
โ V |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ
โ
V) |
74 | 3, 73 | fczfsuppd 9331 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ต ร {โ
}) finSupp
โ
) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ต ร {โ
}) finSupp
โ
) |
76 | 1, 2, 3 | cantnfs 9610 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ต ร {โ
}) โ ๐ โ ((๐ต ร {โ
}):๐ตโถ๐ด โง (๐ต ร {โ
}) finSupp
โ
))) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ((๐ต ร {โ
}) โ ๐ โ ((๐ต ร {โ
}):๐ตโถ๐ด โง (๐ต ร {โ
}) finSupp
โ
))) |
78 | 71, 75, 77 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ต ร {โ
}) โ ๐) |
79 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
) |
80 | 1, 33, 35, 54, 78, 79 | cantnfval 9612 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) =
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , โ
)โ๐)) ยทo ((๐ต ร {โ
})โ(OrdIso( E ,
โ
)โ๐)))
+o ๐ง)),
โ
)โdom OrdIso( E , โ
))) |
81 | | we0 5632 |
. . . . . . . . . . . . . . . . . . . . . 22
โข E We
โ
|
82 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข OrdIso( E
, โ
) = OrdIso( E , โ
) |
83 | 82 | oien 9482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((โ
โ V โง E We โ
) โ dom OrdIso( E , โ
) โ
โ
) |
84 | 72, 81, 83 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
โข dom
OrdIso( E , โ
) โ โ
|
85 | | en0 8963 |
. . . . . . . . . . . . . . . . . . . . 21
โข (dom
OrdIso( E , โ
) โ โ
โ dom OrdIso( E , โ
) =
โ
) |
86 | 84, 85 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . 20
โข dom
OrdIso( E , โ
) = โ
|
87 | 86 | fveq2i 6849 |
. . . . . . . . . . . . . . . . . . 19
โข
(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , โ
))
= (seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , โ
)โ๐)) ยทo ((๐ต ร {โ
})โ(OrdIso( E ,
โ
)โ๐)))
+o ๐ง)),
โ
)โโ
) |
88 | 79 | seqom0g 8406 |
. . . . . . . . . . . . . . . . . . . 20
โข (โ
โ V โ (seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
)โโ
) =
โ
) |
89 | 72, 88 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข
(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
)โโ
) =
โ
|
90 | 87, 89 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
โข
(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E ,
โ
)โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , โ
)โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , โ
))
= โ
|
91 | 80, 90 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) =
โ
) |
92 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
93 | 92 | ffnd 6673 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ (๐ด CNF ๐ต) Fn ๐) |
94 | | fnfvelrn 7035 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด CNF ๐ต) Fn ๐ โง (๐ต ร {โ
}) โ ๐) โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) โ ran (๐ด CNF ๐ต)) |
95 | 93, 78, 94 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) โ ran (๐ด CNF ๐ต)) |
96 | 91, 95 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ โ
โ ran (๐ด CNF ๐ต)) |
97 | 32, 50, 96 | pm2.61ne 3027 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ก โ (๐ด โo ๐ต) โง ๐ก โ ran (๐ด CNF ๐ต))) โ ๐ก โ ran (๐ด CNF ๐ต)) |
98 | 97 | expr 458 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ก โ (๐ด โo ๐ต)) โ (๐ก โ ran (๐ด CNF ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต))) |
99 | 31, 98 | sylbid 239 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ก โ (๐ด โo ๐ต)) โ (โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ ๐ก โ ran (๐ด CNF ๐ต))) |
100 | 99 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (๐ก โ (๐ด โo ๐ต) โ (โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ ๐ก โ ran (๐ด CNF ๐ต)))) |
101 | 100 | com23 86 |
. . . . . . . . . . 11
โข (๐ โ (โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต)) โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต)))) |
102 | 101 | a2i 14 |
. . . . . . . . . 10
โข ((๐ โ โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))) โ (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต)))) |
103 | 102 | a1i 11 |
. . . . . . . . 9
โข (๐ก โ On โ ((๐ โ โ๐ฆ โ ๐ก (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))) โ (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต))))) |
104 | 23, 103 | biimtrid 241 |
. . . . . . . 8
โข (๐ก โ On โ (โ๐ฆ โ ๐ก (๐ โ (๐ฆ โ (๐ด โo ๐ต) โ ๐ฆ โ ran (๐ด CNF ๐ต))) โ (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต))))) |
105 | 22, 104 | tfis2 7797 |
. . . . . . 7
โข (๐ก โ On โ (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต)))) |
106 | 105 | com3l 89 |
. . . . . 6
โข (๐ โ (๐ก โ (๐ด โo ๐ต) โ (๐ก โ On โ ๐ก โ ran (๐ด CNF ๐ต)))) |
107 | 18, 106 | mpdd 43 |
. . . . 5
โข (๐ โ (๐ก โ (๐ด โo ๐ต) โ ๐ก โ ran (๐ด CNF ๐ต))) |
108 | 107 | ssrdv 3954 |
. . . 4
โข (๐ โ (๐ด โo ๐ต) โ ran (๐ด CNF ๐ต)) |
109 | 15, 108 | eqssd 3965 |
. . 3
โข (๐ โ ran (๐ด CNF ๐ต) = (๐ด โo ๐ต)) |
110 | | dffo2 6764 |
. . 3
โข ((๐ด CNF ๐ต):๐โontoโ(๐ด โo ๐ต) โ ((๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต) โง ran (๐ด CNF ๐ต) = (๐ด โo ๐ต))) |
111 | 14, 109, 110 | sylanbrc 584 |
. 2
โข (๐ โ (๐ด CNF ๐ต):๐โontoโ(๐ด โo ๐ต)) |
112 | 2 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ๐ด โ On) |
113 | 3 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ๐ต โ On) |
114 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ง = ๐ก โ (๐ฅโ๐ง) = (๐ฅโ๐ก)) |
115 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ง = ๐ก โ (๐ฆโ๐ง) = (๐ฆโ๐ก)) |
116 | 114, 115 | eleq12d 2828 |
. . . . . . . . . . 11
โข (๐ง = ๐ก โ ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โ (๐ฅโ๐ก) โ (๐ฆโ๐ก))) |
117 | | eleq1w 2817 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ก โ (๐ง โ ๐ค โ ๐ก โ ๐ค)) |
118 | 117 | imbi1d 342 |
. . . . . . . . . . . 12
โข (๐ง = ๐ก โ ((๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)) โ (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))) |
119 | 118 | ralbidv 3171 |
. . . . . . . . . . 11
โข (๐ง = ๐ก โ (โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)) โ โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))) |
120 | 116, 119 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ง = ๐ก โ (((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))) โ ((๐ฅโ๐ก) โ (๐ฆโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))))) |
121 | 120 | cbvrexvw 3225 |
. . . . . . . . 9
โข
(โ๐ง โ
๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))) โ โ๐ก โ ๐ต ((๐ฅโ๐ก) โ (๐ฆโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))) |
122 | | fveq1 6845 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ข โ (๐ฅโ๐ก) = (๐ขโ๐ก)) |
123 | | fveq1 6845 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ฃ โ (๐ฆโ๐ก) = (๐ฃโ๐ก)) |
124 | | eleq12 2824 |
. . . . . . . . . . . 12
โข (((๐ฅโ๐ก) = (๐ขโ๐ก) โง (๐ฆโ๐ก) = (๐ฃโ๐ก)) โ ((๐ฅโ๐ก) โ (๐ฆโ๐ก) โ (๐ขโ๐ก) โ (๐ฃโ๐ก))) |
125 | 122, 123,
124 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ ((๐ฅโ๐ก) โ (๐ฆโ๐ก) โ (๐ขโ๐ก) โ (๐ฃโ๐ก))) |
126 | | fveq1 6845 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ข โ (๐ฅโ๐ค) = (๐ขโ๐ค)) |
127 | | fveq1 6845 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ฃ โ (๐ฆโ๐ค) = (๐ฃโ๐ค)) |
128 | 126, 127 | eqeqan12d 2747 |
. . . . . . . . . . . . 13
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ ((๐ฅโ๐ค) = (๐ฆโ๐ค) โ (๐ขโ๐ค) = (๐ฃโ๐ค))) |
129 | 128 | imbi2d 341 |
. . . . . . . . . . . 12
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ ((๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)) โ (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค)))) |
130 | 129 | ralbidv 3171 |
. . . . . . . . . . 11
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ (โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)) โ โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค)))) |
131 | 125, 130 | anbi12d 632 |
. . . . . . . . . 10
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ (((๐ฅโ๐ก) โ (๐ฆโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))) โ ((๐ขโ๐ก) โ (๐ฃโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค))))) |
132 | 131 | rexbidv 3172 |
. . . . . . . . 9
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ (โ๐ก โ ๐ต ((๐ฅโ๐ก) โ (๐ฆโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))) โ โ๐ก โ ๐ต ((๐ขโ๐ก) โ (๐ฃโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค))))) |
133 | 121, 132 | bitrid 283 |
. . . . . . . 8
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ (โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค))) โ โ๐ก โ ๐ต ((๐ขโ๐ก) โ (๐ฃโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค))))) |
134 | 133 | cbvopabv 5182 |
. . . . . . 7
โข
{โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} = {โจ๐ข, ๐ฃโฉ โฃ โ๐ก โ ๐ต ((๐ขโ๐ก) โ (๐ฃโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค)))} |
135 | 4, 134 | eqtri 2761 |
. . . . . 6
โข ๐ = {โจ๐ข, ๐ฃโฉ โฃ โ๐ก โ ๐ต ((๐ขโ๐ก) โ (๐ฃโ๐ก) โง โ๐ค โ ๐ต (๐ก โ ๐ค โ (๐ขโ๐ค) = (๐ฃโ๐ค)))} |
136 | | simprll 778 |
. . . . . 6
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ๐ โ ๐) |
137 | | simprlr 779 |
. . . . . 6
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ๐ โ ๐) |
138 | | simprr 772 |
. . . . . 6
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ๐๐๐) |
139 | | eqid 2733 |
. . . . . 6
โข โช {๐
โ ๐ต โฃ (๐โ๐) โ (๐โ๐)} = โช {๐ โ ๐ต โฃ (๐โ๐) โ (๐โ๐)} |
140 | | eqid 2733 |
. . . . . 6
โข OrdIso( E
, (๐ supp โ
)) =
OrdIso( E , (๐ supp
โ
)) |
141 | | eqid 2733 |
. . . . . 6
โข
seqฯ((๐ โ V, ๐ก โ V โฆ (((๐ด โo (OrdIso( E , (๐ supp โ
))โ๐)) ยทo (๐โ(OrdIso( E , (๐ supp โ
))โ๐))) +o ๐ก)), โ
) =
seqฯ((๐
โ V, ๐ก โ V
โฆ (((๐ด
โo (OrdIso( E , (๐ supp โ
))โ๐)) ยทo (๐โ(OrdIso( E , (๐ supp โ
))โ๐))) +o ๐ก)), โ
) |
142 | 1, 112, 113, 135, 136, 137, 138, 139, 140, 141 | cantnflem1 9633 |
. . . . 5
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ((๐ด CNF ๐ต)โ๐) โ ((๐ด CNF ๐ต)โ๐)) |
143 | | fvex 6859 |
. . . . . 6
โข ((๐ด CNF ๐ต)โ๐) โ V |
144 | 143 | epeli 5543 |
. . . . 5
โข (((๐ด CNF ๐ต)โ๐) E ((๐ด CNF ๐ต)โ๐) โ ((๐ด CNF ๐ต)โ๐) โ ((๐ด CNF ๐ต)โ๐)) |
145 | 142, 144 | sylibr 233 |
. . . 4
โข ((๐ โง ((๐ โ ๐ โง ๐ โ ๐) โง ๐๐๐)) โ ((๐ด CNF ๐ต)โ๐) E ((๐ด CNF ๐ต)โ๐)) |
146 | 145 | expr 458 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐ โ ((๐ด CNF ๐ต)โ๐) E ((๐ด CNF ๐ต)โ๐))) |
147 | 146 | ralrimivva 3194 |
. 2
โข (๐ โ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐ โ ((๐ด CNF ๐ต)โ๐) E ((๐ด CNF ๐ต)โ๐))) |
148 | | soisoi 7277 |
. 2
โข (((๐ Or ๐ โง E Po (๐ด โo ๐ต)) โง ((๐ด CNF ๐ต):๐โontoโ(๐ด โo ๐ต) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐ โ ((๐ด CNF ๐ต)โ๐) E ((๐ด CNF ๐ต)โ๐)))) โ (๐ด CNF ๐ต) Isom ๐, E (๐, (๐ด โo ๐ต))) |
149 | 5, 13, 111, 147, 148 | syl22anc 838 |
1
โข (๐ โ (๐ด CNF ๐ต) Isom ๐, E (๐, (๐ด โo ๐ต))) |