Step | Hyp | Ref
| Expression |
1 | | ovex 7390 |
. . . . . 6
โข (๐บ supp โ
) โ
V |
2 | | cantnflem1.o |
. . . . . . 7
โข ๐ = OrdIso( E , (๐บ supp โ
)) |
3 | 2 | oion 9472 |
. . . . . 6
โข ((๐บ supp โ
) โ V โ
dom ๐ โ
On) |
4 | 1, 3 | mp1i 13 |
. . . . 5
โข (๐ โ dom ๐ โ On) |
5 | | uniexg 7677 |
. . . . 5
โข (dom
๐ โ On โ โช dom ๐ โ V) |
6 | | sucidg 6398 |
. . . . 5
โข (โช dom ๐ โ V โ โช dom ๐ โ suc โช dom
๐) |
7 | 4, 5, 6 | 3syl 18 |
. . . 4
โข (๐ โ โช dom ๐ โ suc โช dom
๐) |
8 | | cantnfs.s |
. . . . . . . . . 10
โข ๐ = dom (๐ด CNF ๐ต) |
9 | | cantnfs.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ On) |
10 | | cantnfs.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ On) |
11 | | oemapval.t |
. . . . . . . . . 10
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ต ((๐ฅโ๐ง) โ (๐ฆโ๐ง) โง โ๐ค โ ๐ต (๐ง โ ๐ค โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} |
12 | | oemapval.f |
. . . . . . . . . 10
โข (๐ โ ๐น โ ๐) |
13 | | oemapval.g |
. . . . . . . . . 10
โข (๐ โ ๐บ โ ๐) |
14 | | oemapvali.r |
. . . . . . . . . 10
โข (๐ โ ๐น๐๐บ) |
15 | | oemapvali.x |
. . . . . . . . . 10
โข ๐ = โช
{๐ โ ๐ต โฃ (๐นโ๐) โ (๐บโ๐)} |
16 | 8, 9, 10, 11, 12, 13, 14, 15 | cantnflem1a 9621 |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐บ supp โ
)) |
17 | | n0i 4293 |
. . . . . . . . 9
โข (๐ โ (๐บ supp โ
) โ ยฌ (๐บ supp โ
) =
โ
) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
โข (๐ โ ยฌ (๐บ supp โ
) = โ
) |
19 | | ovexd 7392 |
. . . . . . . . . 10
โข (๐ โ (๐บ supp โ
) โ V) |
20 | 8, 9, 10, 2, 13 | cantnfcl 9603 |
. . . . . . . . . . 11
โข (๐ โ ( E We (๐บ supp โ
) โง dom ๐ โ ฯ)) |
21 | 20 | simpld 495 |
. . . . . . . . . 10
โข (๐ โ E We (๐บ supp โ
)) |
22 | 2 | oien 9474 |
. . . . . . . . . 10
โข (((๐บ supp โ
) โ V โง E
We (๐บ supp โ
)) โ
dom ๐ โ (๐บ supp โ
)) |
23 | 19, 21, 22 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ dom ๐ โ (๐บ supp โ
)) |
24 | | breq1 5108 |
. . . . . . . . . 10
โข (dom
๐ = โ
โ (dom
๐ โ (๐บ supp โ
) โ โ
โ (๐บ supp
โ
))) |
25 | | ensymb 8942 |
. . . . . . . . . . 11
โข (โ
โ (๐บ supp โ
)
โ (๐บ supp โ
)
โ โ
) |
26 | | en0 8957 |
. . . . . . . . . . 11
โข ((๐บ supp โ
) โ โ
โ (๐บ supp โ
) =
โ
) |
27 | 25, 26 | bitri 274 |
. . . . . . . . . 10
โข (โ
โ (๐บ supp โ
)
โ (๐บ supp โ
) =
โ
) |
28 | 24, 27 | bitrdi 286 |
. . . . . . . . 9
โข (dom
๐ = โ
โ (dom
๐ โ (๐บ supp โ
) โ (๐บ supp โ
) =
โ
)) |
29 | 23, 28 | syl5ibcom 244 |
. . . . . . . 8
โข (๐ โ (dom ๐ = โ
โ (๐บ supp โ
) = โ
)) |
30 | 18, 29 | mtod 197 |
. . . . . . 7
โข (๐ โ ยฌ dom ๐ = โ
) |
31 | 20 | simprd 496 |
. . . . . . . 8
โข (๐ โ dom ๐ โ ฯ) |
32 | | nnlim 7816 |
. . . . . . . 8
โข (dom
๐ โ ฯ โ
ยฌ Lim dom ๐) |
33 | 31, 32 | syl 17 |
. . . . . . 7
โข (๐ โ ยฌ Lim dom ๐) |
34 | | ioran 982 |
. . . . . . 7
โข (ยฌ
(dom ๐ = โ
โจ Lim
dom ๐) โ (ยฌ dom
๐ = โ
โง ยฌ Lim
dom ๐)) |
35 | 30, 33, 34 | sylanbrc 583 |
. . . . . 6
โข (๐ โ ยฌ (dom ๐ = โ
โจ Lim dom ๐)) |
36 | 2 | oicl 9465 |
. . . . . . 7
โข Ord dom
๐ |
37 | | unizlim 6440 |
. . . . . . 7
โข (Ord dom
๐ โ (dom ๐ = โช
dom ๐ โ (dom ๐ = โ
โจ Lim dom ๐))) |
38 | 36, 37 | mp1i 13 |
. . . . . 6
โข (๐ โ (dom ๐ = โช dom ๐ โ (dom ๐ = โ
โจ Lim dom ๐))) |
39 | 35, 38 | mtbird 324 |
. . . . 5
โข (๐ โ ยฌ dom ๐ = โช
dom ๐) |
40 | | orduniorsuc 7765 |
. . . . . . 7
โข (Ord dom
๐ โ (dom ๐ = โช
dom ๐ โจ dom ๐ = suc โช dom ๐)) |
41 | 36, 40 | mp1i 13 |
. . . . . 6
โข (๐ โ (dom ๐ = โช dom ๐ โจ dom ๐ = suc โช dom
๐)) |
42 | 41 | ord 862 |
. . . . 5
โข (๐ โ (ยฌ dom ๐ = โช
dom ๐ โ dom ๐ = suc โช dom ๐)) |
43 | 39, 42 | mpd 15 |
. . . 4
โข (๐ โ dom ๐ = suc โช dom
๐) |
44 | 7, 43 | eleqtrrd 2840 |
. . 3
โข (๐ โ โช dom ๐ โ dom ๐) |
45 | 2 | oiiso 9473 |
. . . . . . . 8
โข (((๐บ supp โ
) โ V โง E
We (๐บ supp โ
)) โ
๐ Isom E , E (dom ๐, (๐บ supp โ
))) |
46 | 19, 21, 45 | syl2anc 584 |
. . . . . . 7
โข (๐ โ ๐ Isom E , E (dom ๐, (๐บ supp โ
))) |
47 | | isof1o 7268 |
. . . . . . 7
โข (๐ Isom E , E (dom ๐, (๐บ supp โ
)) โ ๐:dom ๐โ1-1-ontoโ(๐บ supp โ
)) |
48 | 46, 47 | syl 17 |
. . . . . 6
โข (๐ โ ๐:dom ๐โ1-1-ontoโ(๐บ supp โ
)) |
49 | | f1ocnv 6796 |
. . . . . 6
โข (๐:dom ๐โ1-1-ontoโ(๐บ supp โ
) โ โก๐:(๐บ supp โ
)โ1-1-ontoโdom
๐) |
50 | | f1of 6784 |
. . . . . 6
โข (โก๐:(๐บ supp โ
)โ1-1-ontoโdom
๐ โ โก๐:(๐บ supp โ
)โถdom ๐) |
51 | 48, 49, 50 | 3syl 18 |
. . . . 5
โข (๐ โ โก๐:(๐บ supp โ
)โถdom ๐) |
52 | 51, 16 | ffvelcdmd 7036 |
. . . 4
โข (๐ โ (โก๐โ๐) โ dom ๐) |
53 | | elssuni 4898 |
. . . 4
โข ((โก๐โ๐) โ dom ๐ โ (โก๐โ๐) โ โช dom
๐) |
54 | 52, 53 | syl 17 |
. . 3
โข (๐ โ (โก๐โ๐) โ โช dom
๐) |
55 | 43, 31 | eqeltrrd 2838 |
. . . . 5
โข (๐ โ suc โช dom ๐ โ ฯ) |
56 | | peano2b 7819 |
. . . . 5
โข (โช dom ๐ โ ฯ โ suc โช dom ๐ โ ฯ) |
57 | 55, 56 | sylibr 233 |
. . . 4
โข (๐ โ โช dom ๐ โ ฯ) |
58 | | eleq1 2825 |
. . . . . . . 8
โข (๐ฆ = โช
dom ๐ โ (๐ฆ โ dom ๐ โ โช dom
๐ โ dom ๐)) |
59 | | sseq2 3970 |
. . . . . . . 8
โข (๐ฆ = โช
dom ๐ โ ((โก๐โ๐) โ ๐ฆ โ (โก๐โ๐) โ โช dom
๐)) |
60 | 58, 59 | anbi12d 631 |
. . . . . . 7
โข (๐ฆ = โช
dom ๐ โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ (โช dom
๐ โ dom ๐ โง (โก๐โ๐) โ โช dom
๐))) |
61 | | fveq2 6842 |
. . . . . . . . . . . 12
โข (๐ฆ = โช
dom ๐ โ (๐โ๐ฆ) = (๐โโช dom
๐)) |
62 | 61 | sseq2d 3976 |
. . . . . . . . . . 11
โข (๐ฆ = โช
dom ๐ โ (๐ฅ โ (๐โ๐ฆ) โ ๐ฅ โ (๐โโช dom
๐))) |
63 | 62 | ifbid 4509 |
. . . . . . . . . 10
โข (๐ฆ = โช
dom ๐ โ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
)) |
64 | 63 | mpteq2dv 5207 |
. . . . . . . . 9
โข (๐ฆ = โช
dom ๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) |
65 | 64 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = โช
dom ๐ โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
)))) |
66 | | suceq 6383 |
. . . . . . . . 9
โข (๐ฆ = โช
dom ๐ โ suc ๐ฆ = suc โช dom ๐) |
67 | 66 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = โช
dom ๐ โ (๐ปโsuc ๐ฆ) = (๐ปโsuc โช dom
๐)) |
68 | 65, 67 | eleq12d 2831 |
. . . . . . 7
โข (๐ฆ = โช
dom ๐ โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐))) |
69 | 60, 68 | imbi12d 344 |
. . . . . 6
โข (๐ฆ = โช
dom ๐ โ (((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ)) โ ((โช dom
๐ โ dom ๐ โง (โก๐โ๐) โ โช dom
๐) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐)))) |
70 | 69 | imbi2d 340 |
. . . . 5
โข (๐ฆ = โช
dom ๐ โ ((๐ โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ))) โ (๐ โ ((โช dom
๐ โ dom ๐ โง (โก๐โ๐) โ โช dom
๐) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐))))) |
71 | | eleq1 2825 |
. . . . . . . 8
โข (๐ฆ = โ
โ (๐ฆ โ dom ๐ โ โ
โ dom ๐)) |
72 | | sseq2 3970 |
. . . . . . . 8
โข (๐ฆ = โ
โ ((โก๐โ๐) โ ๐ฆ โ (โก๐โ๐) โ โ
)) |
73 | 71, 72 | anbi12d 631 |
. . . . . . 7
โข (๐ฆ = โ
โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ (โ
โ dom ๐ โง (โก๐โ๐) โ โ
))) |
74 | | fveq2 6842 |
. . . . . . . . . . . 12
โข (๐ฆ = โ
โ (๐โ๐ฆ) = (๐โโ
)) |
75 | 74 | sseq2d 3976 |
. . . . . . . . . . 11
โข (๐ฆ = โ
โ (๐ฅ โ (๐โ๐ฆ) โ ๐ฅ โ (๐โโ
))) |
76 | 75 | ifbid 4509 |
. . . . . . . . . 10
โข (๐ฆ = โ
โ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
)) |
77 | 76 | mpteq2dv 5207 |
. . . . . . . . 9
โข (๐ฆ = โ
โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) |
78 | 77 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = โ
โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
)))) |
79 | | suceq 6383 |
. . . . . . . . 9
โข (๐ฆ = โ
โ suc ๐ฆ = suc โ
) |
80 | 79 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = โ
โ (๐ปโsuc ๐ฆ) = (๐ปโsuc โ
)) |
81 | 78, 80 | eleq12d 2831 |
. . . . . . 7
โข (๐ฆ = โ
โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โ
))) |
82 | 73, 81 | imbi12d 344 |
. . . . . 6
โข (๐ฆ = โ
โ (((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ)) โ ((โ
โ dom ๐ โง (โก๐โ๐) โ โ
) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โ
)))) |
83 | | eleq1 2825 |
. . . . . . . 8
โข (๐ฆ = ๐ข โ (๐ฆ โ dom ๐ โ ๐ข โ dom ๐)) |
84 | | sseq2 3970 |
. . . . . . . 8
โข (๐ฆ = ๐ข โ ((โก๐โ๐) โ ๐ฆ โ (โก๐โ๐) โ ๐ข)) |
85 | 83, 84 | anbi12d 631 |
. . . . . . 7
โข (๐ฆ = ๐ข โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ (๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข))) |
86 | | fveq2 6842 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ข โ (๐โ๐ฆ) = (๐โ๐ข)) |
87 | 86 | sseq2d 3976 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ข โ (๐ฅ โ (๐โ๐ฆ) โ ๐ฅ โ (๐โ๐ข))) |
88 | 87 | ifbid 4509 |
. . . . . . . . . 10
โข (๐ฆ = ๐ข โ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) |
89 | 88 | mpteq2dv 5207 |
. . . . . . . . 9
โข (๐ฆ = ๐ข โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) |
90 | 89 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = ๐ข โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)))) |
91 | | suceq 6383 |
. . . . . . . . 9
โข (๐ฆ = ๐ข โ suc ๐ฆ = suc ๐ข) |
92 | 91 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = ๐ข โ (๐ปโsuc ๐ฆ) = (๐ปโsuc ๐ข)) |
93 | 90, 92 | eleq12d 2831 |
. . . . . . 7
โข (๐ฆ = ๐ข โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข))) |
94 | 85, 93 | imbi12d 344 |
. . . . . 6
โข (๐ฆ = ๐ข โ (((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ)) โ ((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)))) |
95 | | eleq1 2825 |
. . . . . . . 8
โข (๐ฆ = suc ๐ข โ (๐ฆ โ dom ๐ โ suc ๐ข โ dom ๐)) |
96 | | sseq2 3970 |
. . . . . . . 8
โข (๐ฆ = suc ๐ข โ ((โก๐โ๐) โ ๐ฆ โ (โก๐โ๐) โ suc ๐ข)) |
97 | 95, 96 | anbi12d 631 |
. . . . . . 7
โข (๐ฆ = suc ๐ข โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ suc ๐ข))) |
98 | | fveq2 6842 |
. . . . . . . . . . . 12
โข (๐ฆ = suc ๐ข โ (๐โ๐ฆ) = (๐โsuc ๐ข)) |
99 | 98 | sseq2d 3976 |
. . . . . . . . . . 11
โข (๐ฆ = suc ๐ข โ (๐ฅ โ (๐โ๐ฆ) โ ๐ฅ โ (๐โsuc ๐ข))) |
100 | 99 | ifbid 4509 |
. . . . . . . . . 10
โข (๐ฆ = suc ๐ข โ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
)) |
101 | 100 | mpteq2dv 5207 |
. . . . . . . . 9
โข (๐ฆ = suc ๐ข โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) |
102 | 101 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = suc ๐ข โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
)))) |
103 | | suceq 6383 |
. . . . . . . . 9
โข (๐ฆ = suc ๐ข โ suc ๐ฆ = suc suc ๐ข) |
104 | 103 | fveq2d 6846 |
. . . . . . . 8
โข (๐ฆ = suc ๐ข โ (๐ปโsuc ๐ฆ) = (๐ปโsuc suc ๐ข)) |
105 | 102, 104 | eleq12d 2831 |
. . . . . . 7
โข (๐ฆ = suc ๐ข โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
106 | 97, 105 | imbi12d 344 |
. . . . . 6
โข (๐ฆ = suc ๐ข โ (((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ)) โ ((suc ๐ข โ dom ๐ โง (โก๐โ๐) โ suc ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
107 | | f1ocnvfv2 7223 |
. . . . . . . . . . . . 13
โข ((๐:dom ๐โ1-1-ontoโ(๐บ supp โ
) โง ๐ โ (๐บ supp โ
)) โ (๐โ(โก๐โ๐)) = ๐) |
108 | 48, 16, 107 | syl2anc 584 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ(โก๐โ๐)) = ๐) |
109 | 108 | sseq2d 3976 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ (๐โ(โก๐โ๐)) โ ๐ฅ โ ๐)) |
110 | 109 | ifbid 4509 |
. . . . . . . . . 10
โข (๐ โ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
) = if(๐ฅ โ ๐, (๐นโ๐ฅ), โ
)) |
111 | 110 | mpteq2dv 5207 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ ๐, (๐นโ๐ฅ), โ
))) |
112 | 111 | fveq2d 6846 |
. . . . . . . 8
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ ๐, (๐นโ๐ฅ), โ
)))) |
113 | | cantnflem1.h |
. . . . . . . . 9
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐โ๐)) ยทo (๐บโ(๐โ๐))) +o ๐ง)), โ
) |
114 | 8, 9, 10, 11, 12, 13, 14, 15, 2, 113 | cantnflem1d 9624 |
. . . . . . . 8
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ ๐, (๐นโ๐ฅ), โ
))) โ (๐ปโsuc (โก๐โ๐))) |
115 | 112, 114 | eqeltrd 2837 |
. . . . . . 7
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc (โก๐โ๐))) |
116 | | ss0 4358 |
. . . . . . . . . . . . . 14
โข ((โก๐โ๐) โ โ
โ (โก๐โ๐) = โ
) |
117 | 116 | fveq2d 6846 |
. . . . . . . . . . . . 13
โข ((โก๐โ๐) โ โ
โ (๐โ(โก๐โ๐)) = (๐โโ
)) |
118 | 117 | sseq2d 3976 |
. . . . . . . . . . . 12
โข ((โก๐โ๐) โ โ
โ (๐ฅ โ (๐โ(โก๐โ๐)) โ ๐ฅ โ (๐โโ
))) |
119 | 118 | ifbid 4509 |
. . . . . . . . . . 11
โข ((โก๐โ๐) โ โ
โ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
)) |
120 | 119 | mpteq2dv 5207 |
. . . . . . . . . 10
โข ((โก๐โ๐) โ โ
โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) |
121 | 120 | fveq2d 6846 |
. . . . . . . . 9
โข ((โก๐โ๐) โ โ
โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
)))) |
122 | | suceq 6383 |
. . . . . . . . . . 11
โข ((โก๐โ๐) = โ
โ suc (โก๐โ๐) = suc โ
) |
123 | 116, 122 | syl 17 |
. . . . . . . . . 10
โข ((โก๐โ๐) โ โ
โ suc (โก๐โ๐) = suc โ
) |
124 | 123 | fveq2d 6846 |
. . . . . . . . 9
โข ((โก๐โ๐) โ โ
โ (๐ปโsuc (โก๐โ๐)) = (๐ปโsuc โ
)) |
125 | 121, 124 | eleq12d 2831 |
. . . . . . . 8
โข ((โก๐โ๐) โ โ
โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc (โก๐โ๐)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โ
))) |
126 | 125 | adantl 482 |
. . . . . . 7
โข ((โ
โ dom ๐ โง (โก๐โ๐) โ โ
) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc (โก๐โ๐)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โ
))) |
127 | 115, 126 | syl5ibcom 244 |
. . . . . 6
โข (๐ โ ((โ
โ dom ๐ โง (โก๐โ๐) โ โ
) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโ
), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โ
))) |
128 | | ordelon 6341 |
. . . . . . . . . . . 12
โข ((Ord dom
๐ โง (โก๐โ๐) โ dom ๐) โ (โก๐โ๐) โ On) |
129 | 36, 52, 128 | sylancr 587 |
. . . . . . . . . . 11
โข (๐ โ (โก๐โ๐) โ On) |
130 | 36 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ Ord dom ๐) |
131 | | ordelon 6341 |
. . . . . . . . . . . 12
โข ((Ord dom
๐ โง suc ๐ข โ dom ๐) โ suc ๐ข โ On) |
132 | 130, 131 | sylan 580 |
. . . . . . . . . . 11
โข ((๐ โง suc ๐ข โ dom ๐) โ suc ๐ข โ On) |
133 | | onsseleq 6358 |
. . . . . . . . . . 11
โข (((โก๐โ๐) โ On โง suc ๐ข โ On) โ ((โก๐โ๐) โ suc ๐ข โ ((โก๐โ๐) โ suc ๐ข โจ (โก๐โ๐) = suc ๐ข))) |
134 | 129, 132,
133 | syl2an2r 683 |
. . . . . . . . . 10
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) โ suc ๐ข โ ((โก๐โ๐) โ suc ๐ข โจ (โก๐โ๐) = suc ๐ข))) |
135 | | onsucb 7752 |
. . . . . . . . . . . . . . 15
โข (๐ข โ On โ suc ๐ข โ On) |
136 | 132, 135 | sylibr 233 |
. . . . . . . . . . . . . 14
โข ((๐ โง suc ๐ข โ dom ๐) โ ๐ข โ On) |
137 | | eloni 6327 |
. . . . . . . . . . . . . 14
โข (๐ข โ On โ Ord ๐ข) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง suc ๐ข โ dom ๐) โ Ord ๐ข) |
139 | | ordsssuc 6406 |
. . . . . . . . . . . . 13
โข (((โก๐โ๐) โ On โง Ord ๐ข) โ ((โก๐โ๐) โ ๐ข โ (โก๐โ๐) โ suc ๐ข)) |
140 | 129, 138,
139 | syl2an2r 683 |
. . . . . . . . . . . 12
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) โ ๐ข โ (โก๐โ๐) โ suc ๐ข)) |
141 | | ordtr 6331 |
. . . . . . . . . . . . . . . . 17
โข (Ord dom
๐ โ Tr dom ๐) |
142 | 36, 141 | mp1i 13 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ Tr dom ๐) |
143 | | simprl 769 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ suc ๐ข โ dom ๐) |
144 | | trsuc 6404 |
. . . . . . . . . . . . . . . 16
โข ((Tr dom
๐ โง suc ๐ข โ dom ๐) โ ๐ข โ dom ๐) |
145 | 142, 143,
144 | syl2anc 584 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ข โ dom ๐) |
146 | | simprr 771 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (โก๐โ๐) โ ๐ข) |
147 | 145, 146 | jca 512 |
. . . . . . . . . . . . . 14
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) |
148 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ต โ On) |
149 | | oecl 8483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
150 | 9, 148, 149 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ด โo ๐ต) โ On) |
151 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ด โ On) |
152 | 8, 151, 148 | cantnff 9610 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ด CNF ๐ต):๐โถ(๐ด โo ๐ต)) |
153 | 8, 9, 10 | cantnfs 9602 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐น โ ๐ โ (๐น:๐ตโถ๐ด โง ๐น finSupp โ
))) |
154 | 12, 153 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (๐น:๐ตโถ๐ด โง ๐น finSupp โ
)) |
155 | 154 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ๐น:๐ตโถ๐ด) |
156 | 155 | ffvelcdmda 7035 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐นโ๐ฅ) โ ๐ด) |
157 | 8, 9, 10 | cantnfs 9602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ (๐บ โ ๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
))) |
158 | 13, 157 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ (๐บ:๐ตโถ๐ด โง ๐บ finSupp โ
)) |
159 | 158 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ ๐บ:๐ตโถ๐ด) |
160 | 8, 9, 10, 11, 12, 13, 14, 15 | oemapvali 9620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ (๐ โ ๐ต โง (๐นโ๐) โ (๐บโ๐) โง โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค)))) |
161 | 160 | simp1d 1142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ ๐ โ ๐ต) |
162 | 159, 161 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐บโ๐) โ ๐ด) |
163 | 162 | ne0d 4295 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ๐ด โ โ
) |
164 | | on0eln0 6373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ด โ On โ (โ
โ ๐ด โ ๐ด โ โ
)) |
165 | 9, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (โ
โ ๐ด โ ๐ด โ โ
)) |
166 | 163, 165 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ
โ ๐ด) |
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ ๐ต) โ โ
โ ๐ด) |
168 | 156, 167 | ifcld 4532 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ ๐ต) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ ๐ด) |
169 | 168 | fmpttd 7063 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)):๐ตโถ๐ด) |
170 | 10 | mptexd 7174 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) โ V) |
171 | | funmpt 6539 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข Fun
(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ Fun (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) |
173 | 154 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐น finSupp โ
) |
174 | | ssidd 3967 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐น supp โ
) โ (๐น supp โ
)) |
175 | | 0ex 5264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข โ
โ V |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ
โ
V) |
177 | 155, 174,
10, 176 | suppssr 8127 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง ๐ฅ โ (๐ต โ (๐น supp โ
))) โ (๐นโ๐ฅ) = โ
) |
178 | 177 | ifeq1d 4505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง ๐ฅ โ (๐ต โ (๐น supp โ
))) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โ๐ข), โ
, โ
)) |
179 | | ifid 4526 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข if(๐ฅ โ (๐โ๐ข), โ
, โ
) =
โ
|
180 | 178, 179 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ (๐ต โ (๐น supp โ
))) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = โ
) |
181 | 180, 10 | suppss2 8131 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) โ (๐น supp โ
)) |
182 | | fsuppsssupp 9321 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) โ V โง Fun (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โง (๐น finSupp โ
โง ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) โ (๐น supp โ
))) โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) finSupp
โ
) |
183 | 170, 172,
173, 181, 182 | syl22anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) finSupp
โ
) |
184 | 8, 9, 10 | cantnfs 9602 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) โ ๐ โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)):๐ตโถ๐ด โง (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) finSupp
โ
))) |
185 | 169, 183,
184 | mpbir2and 711 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) โ ๐) |
186 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) โ ๐) |
187 | 152, 186 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ด โo ๐ต)) |
188 | | onelon 6342 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โo ๐ต) โ On โง ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ด โo ๐ต)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ On) |
189 | 150, 187,
188 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ On) |
190 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ dom ๐ โ ฯ) |
191 | | elnn 7813 |
. . . . . . . . . . . . . . . . . . 19
โข ((suc
๐ข โ dom ๐ โง dom ๐ โ ฯ) โ suc ๐ข โ
ฯ) |
192 | 143, 190,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ suc ๐ข โ ฯ) |
193 | 113 | cantnfvalf 9601 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ป:ฯโถOn |
194 | 193 | ffvelcdmi 7034 |
. . . . . . . . . . . . . . . . . 18
โข (suc
๐ข โ ฯ โ
(๐ปโsuc ๐ข) โ On) |
195 | 192, 194 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ปโsuc ๐ข) โ On) |
196 | | suppssdm 8108 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐บ supp โ
) โ dom ๐บ |
197 | 196, 159 | fssdm 6688 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐บ supp โ
) โ ๐ต) |
198 | 197 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐บ supp โ
) โ ๐ต) |
199 | 2 | oif 9466 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐:dom ๐โถ(๐บ supp โ
) |
200 | 199 | ffvelcdmi 7034 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (suc
๐ข โ dom ๐ โ (๐โsuc ๐ข) โ (๐บ supp โ
)) |
201 | 143, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โsuc ๐ข) โ (๐บ supp โ
)) |
202 | 198, 201 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โsuc ๐ข) โ ๐ต) |
203 | | onelon 6342 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ On โง (๐โsuc ๐ข) โ ๐ต) โ (๐โsuc ๐ข) โ On) |
204 | 10, 202, 203 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โsuc ๐ข) โ On) |
205 | | oecl 8483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ On โง (๐โsuc ๐ข) โ On) โ (๐ด โo (๐โsuc ๐ข)) โ On) |
206 | 9, 204, 205 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ด โo (๐โsuc ๐ข)) โ On) |
207 | 155 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐น:๐ตโถ๐ด) |
208 | 207, 202 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐นโ(๐โsuc ๐ข)) โ ๐ด) |
209 | | onelon 6342 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ On โง (๐นโ(๐โsuc ๐ข)) โ ๐ด) โ (๐นโ(๐โsuc ๐ข)) โ On) |
210 | 9, 208, 209 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐นโ(๐โsuc ๐ข)) โ On) |
211 | | omcl 8482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โo (๐โsuc ๐ข)) โ On โง (๐นโ(๐โsuc ๐ข)) โ On) โ ((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) โ On) |
212 | 206, 210,
211 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) โ On) |
213 | | oaord 8494 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ On โง (๐ปโsuc ๐ข) โ On โง ((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) โ On) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)))) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข)))) |
214 | 189, 195,
212, 213 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)))) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข)))) |
215 | | ifeq1 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐นโ๐ฅ) = โ
โ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โsuc ๐ข), โ
, โ
)) |
216 | | ifid 4526 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข if(๐ฅ โ (๐โsuc ๐ข), โ
, โ
) =
โ
|
217 | 215, 216 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐นโ๐ฅ) = โ
โ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
) = โ
) |
218 | | ifeq1 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐นโ๐ฅ) = โ
โ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
) = if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), โ
, โ
)) |
219 | | ifid 4526 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), โ
, โ
) =
โ
|
220 | 218, 219 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐นโ๐ฅ) = โ
โ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
) = โ
) |
221 | 217, 220 | eqeq12d 2752 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐นโ๐ฅ) = โ
โ (if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
) = if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
) โ โ
=
โ
)) |
222 | | onss 7719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ต โ On โ ๐ต โ On) |
223 | 10, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ต โ On) |
224 | 223 | sselda 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
225 | 224 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ ๐ฅ โ On) |
226 | 204 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (๐โsuc ๐ข) โ On) |
227 | | onsseleq 6358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฅ โ On โง (๐โsuc ๐ข) โ On) โ (๐ฅ โ (๐โsuc ๐ข) โ (๐ฅ โ (๐โsuc ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)))) |
228 | 225, 226,
227 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (๐ฅ โ (๐โsuc ๐ข) โ (๐ฅ โ (๐โsuc ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)))) |
229 | 228 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โsuc ๐ข) โ (๐ฅ โ (๐โsuc ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)))) |
230 | 199 | ffvelcdmi 7034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ข โ dom ๐ โ (๐โ๐ข) โ (๐บ supp โ
)) |
231 | 145, 230 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ๐ข) โ (๐บ supp โ
)) |
232 | 198, 231 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ๐ข) โ ๐ต) |
233 | | onelon 6342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ต โ On โง (๐โ๐ข) โ ๐ต) โ (๐โ๐ข) โ On) |
234 | 10, 232, 233 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ๐ข) โ On) |
235 | 234 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐โ๐ข) โ On) |
236 | | onsssuc 6407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฅ โ On โง (๐โ๐ข) โ On) โ (๐ฅ โ (๐โ๐ข) โ ๐ฅ โ suc (๐โ๐ข))) |
237 | 225, 235,
236 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โ๐ข) โ ๐ฅ โ suc (๐โ๐ข))) |
238 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ๐ข โ V |
239 | 238 | sucid 6399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ๐ข โ suc ๐ข |
240 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ Isom E , E (dom ๐, (๐บ supp โ
))) |
241 | | isorel 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง (๐ข โ dom ๐ โง suc ๐ข โ dom ๐)) โ (๐ข E suc ๐ข โ (๐โ๐ข) E (๐โsuc ๐ข))) |
242 | 240, 145,
143, 241 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ข E suc ๐ข โ (๐โ๐ข) E (๐โsuc ๐ข))) |
243 | 238 | sucex 7741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข suc ๐ข โ V |
244 | 243 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ข E suc ๐ข โ ๐ข โ suc ๐ข) |
245 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐โsuc ๐ข) โ V |
246 | 245 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐โ๐ข) E (๐โsuc ๐ข) โ (๐โ๐ข) โ (๐โsuc ๐ข)) |
247 | 242, 244,
246 | 3bitr3g 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ข โ suc ๐ข โ (๐โ๐ข) โ (๐โsuc ๐ข))) |
248 | 239, 247 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ๐ข) โ (๐โsuc ๐ข)) |
249 | | eloni 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐โsuc ๐ข) โ On โ Ord (๐โsuc ๐ข)) |
250 | 204, 249 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ Ord (๐โsuc ๐ข)) |
251 | | ordelsuc 7755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐โ๐ข) โ On โง Ord (๐โsuc ๐ข)) โ ((๐โ๐ข) โ (๐โsuc ๐ข) โ suc (๐โ๐ข) โ (๐โsuc ๐ข))) |
252 | 234, 250,
251 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐โ๐ข) โ (๐โsuc ๐ข) โ suc (๐โ๐ข) โ (๐โsuc ๐ข))) |
253 | 248, 252 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ suc (๐โ๐ข) โ (๐โsuc ๐ข)) |
254 | 253 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ suc (๐โ๐ข) โ (๐โsuc ๐ข)) |
255 | 254 | sseld 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ suc (๐โ๐ข) โ ๐ฅ โ (๐โsuc ๐ข))) |
256 | 237, 255 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โ๐ข) โ ๐ฅ โ (๐โsuc ๐ข))) |
257 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐โ๐ข) โ ๐ฅ) |
258 | 240 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ๐ Isom E , E (dom ๐, (๐บ supp โ
))) |
259 | 258, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ๐:dom ๐โ1-1-ontoโ(๐บ supp โ
)) |
260 | 8, 9, 10, 11, 12, 13, 14, 15, 2 | cantnflem1c 9623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ๐ฅ โ (๐บ supp โ
)) |
261 | | f1ocnvfv2 7223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐:dom ๐โ1-1-ontoโ(๐บ supp โ
) โง ๐ฅ โ (๐บ supp โ
)) โ (๐โ(โก๐โ๐ฅ)) = ๐ฅ) |
262 | 259, 260,
261 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐โ(โก๐โ๐ฅ)) = ๐ฅ) |
263 | 257, 262 | eleqtrrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐โ๐ข) โ (๐โ(โก๐โ๐ฅ))) |
264 | 145 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ๐ข โ dom ๐) |
265 | 259, 49, 50 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ โก๐:(๐บ supp โ
)โถdom ๐) |
266 | 265, 260 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (โก๐โ๐ฅ) โ dom ๐) |
267 | | isorel 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง (๐ข โ dom ๐ โง (โก๐โ๐ฅ) โ dom ๐)) โ (๐ข E (โก๐โ๐ฅ) โ (๐โ๐ข) E (๐โ(โก๐โ๐ฅ)))) |
268 | 258, 264,
266, 267 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐ข E (โก๐โ๐ฅ) โ (๐โ๐ข) E (๐โ(โก๐โ๐ฅ)))) |
269 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (โก๐โ๐ฅ) โ V |
270 | 269 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ข E (โก๐โ๐ฅ) โ ๐ข โ (โก๐โ๐ฅ)) |
271 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐โ(โก๐โ๐ฅ)) โ V |
272 | 271 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐โ๐ข) E (๐โ(โก๐โ๐ฅ)) โ (๐โ๐ข) โ (๐โ(โก๐โ๐ฅ))) |
273 | 268, 270,
272 | 3bitr3g 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐ข โ (โก๐โ๐ฅ) โ (๐โ๐ข) โ (๐โ(โก๐โ๐ฅ)))) |
274 | 263, 273 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ๐ข โ (โก๐โ๐ฅ)) |
275 | | ordelon 6341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((Ord dom
๐ โง (โก๐โ๐ฅ) โ dom ๐) โ (โก๐โ๐ฅ) โ On) |
276 | 36, 266, 275 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (โก๐โ๐ฅ) โ On) |
277 | | eloni 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((โก๐โ๐ฅ) โ On โ Ord (โก๐โ๐ฅ)) |
278 | 276, 277 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ Ord (โก๐โ๐ฅ)) |
279 | | ordelsuc 7755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ข โ (โก๐โ๐ฅ) โง Ord (โก๐โ๐ฅ)) โ (๐ข โ (โก๐โ๐ฅ) โ suc ๐ข โ (โก๐โ๐ฅ))) |
280 | 274, 278,
279 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (๐ข โ (โก๐โ๐ฅ) โ suc ๐ข โ (โก๐โ๐ฅ))) |
281 | 274, 280 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ suc ๐ข โ (โก๐โ๐ฅ)) |
282 | 143 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ suc ๐ข โ dom ๐) |
283 | 36, 282, 131 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ suc ๐ข โ On) |
284 | | ontri1 6351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((suc
๐ข โ On โง (โก๐โ๐ฅ) โ On) โ (suc ๐ข โ (โก๐โ๐ฅ) โ ยฌ (โก๐โ๐ฅ) โ suc ๐ข)) |
285 | 283, 276,
284 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ (suc ๐ข โ (โก๐โ๐ฅ) โ ยฌ (โก๐โ๐ฅ) โ suc ๐ข)) |
286 | 281, 285 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ยฌ (โก๐โ๐ฅ) โ suc ๐ข) |
287 | | isorel 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง ((โก๐โ๐ฅ) โ dom ๐ โง suc ๐ข โ dom ๐)) โ ((โก๐โ๐ฅ) E suc ๐ข โ (๐โ(โก๐โ๐ฅ)) E (๐โsuc ๐ข))) |
288 | 258, 266,
282, 287 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ((โก๐โ๐ฅ) E suc ๐ข โ (๐โ(โก๐โ๐ฅ)) E (๐โsuc ๐ข))) |
289 | 243 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((โก๐โ๐ฅ) E suc ๐ข โ (โก๐โ๐ฅ) โ suc ๐ข) |
290 | 245 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐โ(โก๐โ๐ฅ)) E (๐โsuc ๐ข) โ (๐โ(โก๐โ๐ฅ)) โ (๐โsuc ๐ข)) |
291 | 288, 289,
290 | 3bitr3g 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ((โก๐โ๐ฅ) โ suc ๐ข โ (๐โ(โก๐โ๐ฅ)) โ (๐โsuc ๐ข))) |
292 | 262 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ((๐โ(โก๐โ๐ฅ)) โ (๐โsuc ๐ข) โ ๐ฅ โ (๐โsuc ๐ข))) |
293 | 291, 292 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ((โก๐โ๐ฅ) โ suc ๐ข โ ๐ฅ โ (๐โsuc ๐ข))) |
294 | 286, 293 | mtbid 323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง ((๐นโ๐ฅ) โ โ
โง (๐โ๐ข) โ ๐ฅ)) โ ยฌ ๐ฅ โ (๐โsuc ๐ข)) |
295 | 294 | expr 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ ((๐โ๐ข) โ ๐ฅ โ ยฌ ๐ฅ โ (๐โsuc ๐ข))) |
296 | 295 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โsuc ๐ข) โ ยฌ (๐โ๐ข) โ ๐ฅ)) |
297 | | ontri1 6351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฅ โ On โง (๐โ๐ข) โ On) โ (๐ฅ โ (๐โ๐ข) โ ยฌ (๐โ๐ข) โ ๐ฅ)) |
298 | 225, 235,
297 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โ๐ข) โ ยฌ (๐โ๐ข) โ ๐ฅ)) |
299 | 296, 298 | sylibrd 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โsuc ๐ข) โ ๐ฅ โ (๐โ๐ข))) |
300 | 256, 299 | impbid 211 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โ๐ข) โ ๐ฅ โ (๐โsuc ๐ข))) |
301 | 300 | orbi1d 915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ ((๐ฅ โ (๐โ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)) โ (๐ฅ โ (๐โsuc ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)))) |
302 | 229, 301 | bitr4d 281 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โsuc ๐ข) โ (๐ฅ โ (๐โ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)))) |
303 | | orcom 868 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ (๐โ๐ข) โจ ๐ฅ = (๐โsuc ๐ข)) โ (๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข))) |
304 | 302, 303 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ (๐ฅ โ (๐โsuc ๐ข) โ (๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)))) |
305 | 304 | ifbid 4509 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โง (๐นโ๐ฅ) โ โ
) โ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
) = if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)) |
306 | | eqidd 2737 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ โ
= โ
) |
307 | 221, 305,
306 | pm2.61ne 3030 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
) = if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)) |
308 | 307 | mpteq2dva 5205 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
))) |
309 | 308 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)))) |
310 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐นโ๐ฅ) โ V |
311 | 310, 175 | ifex 4536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V |
312 | 311 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V) |
313 | 312 | ralrimivw 3147 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ โ๐ฅ โ ๐ต if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V) |
314 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) |
315 | 314 | fnmpt 6641 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(โ๐ฅ โ
๐ต if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) Fn ๐ต) |
316 | 313, 315 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) Fn ๐ต) |
317 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ โ
โ V) |
318 | | suppvalfn 8100 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) = {๐ฆ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) โ โ
}) |
319 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
โฒ๐ฆ๐ต |
320 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
โฒ๐ฅ๐ต |
321 | | nffvmpt1 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
โฒ๐ฅ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) |
322 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
โฒ๐ฅโ
|
323 | 321, 322 | nfne 3045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
โฒ๐ฅ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) โ โ
|
324 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
โฒ๐ฆ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
|
325 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ = ๐ฅ โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) = ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ)) |
326 | 325 | neeq1d 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = ๐ฅ โ (((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) โ โ
โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
)) |
327 | 319, 320,
323, 324, 326 | cbvrabw 3439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข {๐ฆ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) โ โ
} = {๐ฅ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
} |
328 | 318, 327 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) = {๐ฅ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
}) |
329 | 316, 148,
317, 328 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) = {๐ฅ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
}) |
330 | | eqidd 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) |
331 | 311 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V) |
332 | 330, 331 | fvmpt2d 6961 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) = if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) |
333 | 332 | neeq1d 3003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
)) |
334 | 331 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V โง if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
))) |
335 | | dif1o 8446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ 1o)
โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ V โง if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
)) |
336 | 334, 335 | bitr4di 288 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ
1o))) |
337 | 333, 336 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ
1o))) |
338 | 337 | rabbidva 3414 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ {๐ฅ โ ๐ต โฃ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฅ) โ โ
} = {๐ฅ โ ๐ต โฃ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ
1o)}) |
339 | 329, 338 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) = {๐ฅ โ ๐ต โฃ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ
1o)}) |
340 | 311, 335 | mpbiran 707 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ 1o)
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
) |
341 | | ifeq1 4490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐นโ๐ฅ) = โ
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โ๐ข), โ
, โ
)) |
342 | 341, 179 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐นโ๐ฅ) = โ
โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = โ
) |
343 | 342 | necon3i 2976 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ (๐นโ๐ฅ) โ โ
) |
344 | | iffalse 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (ยฌ
๐ฅ โ (๐โ๐ข) โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = โ
) |
345 | 344 | necon1ai 2971 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ ๐ฅ โ (๐โ๐ข)) |
346 | 343, 345 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ ((๐นโ๐ฅ) โ โ
โง ๐ฅ โ (๐โ๐ข))) |
347 | 256 | expimpd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (((๐นโ๐ฅ) โ โ
โง ๐ฅ โ (๐โ๐ข)) โ ๐ฅ โ (๐โsuc ๐ข))) |
348 | 346, 347 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ โ
โ ๐ฅ โ (๐โsuc ๐ข))) |
349 | 340, 348 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต) โ (if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ 1o)
โ ๐ฅ โ (๐โsuc ๐ข))) |
350 | 349 | 3impia 1117 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โง ๐ฅ โ ๐ต โง if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ 1o))
โ ๐ฅ โ (๐โsuc ๐ข)) |
351 | 350 | rabssdv 4032 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ {๐ฅ โ ๐ต โฃ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) โ (V โ 1o)}
โ (๐โsuc ๐ข)) |
352 | 339, 351 | eqsstrd 3982 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)) supp โ
) โ (๐โsuc ๐ข)) |
353 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = ๐ฆ โ (๐ฅ = (๐โsuc ๐ข) โ ๐ฆ = (๐โsuc ๐ข))) |
354 | | sseq1 3969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = ๐ฆ โ (๐ฅ โ (๐โ๐ข) โ ๐ฆ โ (๐โ๐ข))) |
355 | 353, 354 | orbi12d 917 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ๐ฆ โ ((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)) โ (๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)))) |
356 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ๐ฆ โ (๐นโ๐ฅ) = (๐นโ๐ฆ)) |
357 | 355, 356 | ifbieq1d 4510 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ฆ โ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
) = if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
)) |
358 | 357 | cbvmptv 5218 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)) = (๐ฆ โ ๐ต โฆ if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
)) |
359 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = (๐โsuc ๐ข) โ (๐นโ๐ฆ) = (๐นโ(๐โsuc ๐ข))) |
360 | 359 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ ๐ต โง ๐ฆ = (๐โsuc ๐ข)) โ (๐นโ๐ฆ) = (๐นโ(๐โsuc ๐ข))) |
361 | 360 | ifeq1da 4517 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ ๐ต โ if(๐ฆ = (๐โsuc ๐ข), (๐นโ๐ฆ), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ)) = if(๐ฆ = (๐โsuc ๐ข), (๐นโ(๐โsuc ๐ข)), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ))) |
362 | 354, 356 | ifbieq1d 4510 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ = ๐ฆ โ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
) = if(๐ฆ โ (๐โ๐ข), (๐นโ๐ฆ), โ
)) |
363 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐นโ๐ฆ) โ V |
364 | 363, 175 | ifex 4536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข if(๐ฆ โ (๐โ๐ข), (๐นโ๐ฆ), โ
) โ V |
365 | 362, 314,
364 | fvmpt 6948 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ ๐ต โ ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ) = if(๐ฆ โ (๐โ๐ข), (๐นโ๐ฆ), โ
)) |
366 | 365 | ifeq2d 4506 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ โ ๐ต โ if(๐ฆ = (๐โsuc ๐ข), (๐นโ๐ฆ), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ)) = if(๐ฆ = (๐โsuc ๐ข), (๐นโ๐ฆ), if(๐ฆ โ (๐โ๐ข), (๐นโ๐ฆ), โ
))) |
367 | | ifor 4540 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
) = if(๐ฆ = (๐โsuc ๐ข), (๐นโ๐ฆ), if(๐ฆ โ (๐โ๐ข), (๐นโ๐ฆ), โ
)) |
368 | 366, 367 | eqtr4di 2794 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ ๐ต โ if(๐ฆ = (๐โsuc ๐ข), (๐นโ๐ฆ), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ)) = if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
)) |
369 | 361, 368 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ ๐ต โ if(๐ฆ = (๐โsuc ๐ข), (๐นโ(๐โsuc ๐ข)), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ)) = if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
)) |
370 | 369 | mpteq2ia 5208 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ ๐ต โฆ if(๐ฆ = (๐โsuc ๐ข), (๐นโ(๐โsuc ๐ข)), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ))) = (๐ฆ โ ๐ต โฆ if((๐ฆ = (๐โsuc ๐ข) โจ ๐ฆ โ (๐โ๐ข)), (๐นโ๐ฆ), โ
)) |
371 | 358, 370 | eqtr4i 2767 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)) = (๐ฆ โ ๐ต โฆ if(๐ฆ = (๐โsuc ๐ข), (๐นโ(๐โsuc ๐ข)), ((๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))โ๐ฆ))) |
372 | 8, 151, 148, 186, 202, 208, 352, 371 | cantnfp1 9617 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
)) โ ๐ โง ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
))) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)))))) |
373 | 372 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if((๐ฅ = (๐โsuc ๐ข) โจ ๐ฅ โ (๐โ๐ข)), (๐นโ๐ฅ), โ
))) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))))) |
374 | 309, 373 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))))) |
375 | 8, 9, 10, 2, 13, 113 | cantnfsuc 9606 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง suc ๐ข โ ฯ) โ (๐ปโsuc suc ๐ข) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐บโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข))) |
376 | 192, 375 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ปโsuc suc ๐ข) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐บโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข))) |
377 | 160 | simp3d 1144 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค))) |
378 | 377 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค))) |
379 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ(โก๐โ๐)) = ๐) |
380 | 136 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ข โ On) |
381 | | onsssuc 6407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((โก๐โ๐) โ On โง ๐ข โ On) โ ((โก๐โ๐) โ ๐ข โ (โก๐โ๐) โ suc ๐ข)) |
382 | 129, 380,
381 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((โก๐โ๐) โ ๐ข โ (โก๐โ๐) โ suc ๐ข)) |
383 | 146, 382 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (โก๐โ๐) โ suc ๐ข) |
384 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (โก๐โ๐) โ dom ๐) |
385 | | isorel 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง ((โก๐โ๐) โ dom ๐ โง suc ๐ข โ dom ๐)) โ ((โก๐โ๐) E suc ๐ข โ (๐โ(โก๐โ๐)) E (๐โsuc ๐ข))) |
386 | 240, 384,
143, 385 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((โก๐โ๐) E suc ๐ข โ (๐โ(โก๐โ๐)) E (๐โsuc ๐ข))) |
387 | 243 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((โก๐โ๐) E suc ๐ข โ (โก๐โ๐) โ suc ๐ข) |
388 | 245 | epeli 5539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐โ(โก๐โ๐)) E (๐โsuc ๐ข) โ (๐โ(โก๐โ๐)) โ (๐โsuc ๐ข)) |
389 | 386, 387,
388 | 3bitr3g 312 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((โก๐โ๐) โ suc ๐ข โ (๐โ(โก๐โ๐)) โ (๐โsuc ๐ข))) |
390 | 383, 389 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐โ(โก๐โ๐)) โ (๐โsuc ๐ข)) |
391 | 379, 390 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ๐ โ (๐โsuc ๐ข)) |
392 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ค = (๐โsuc ๐ข) โ (๐ โ ๐ค โ ๐ โ (๐โsuc ๐ข))) |
393 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ค = (๐โsuc ๐ข) โ (๐นโ๐ค) = (๐นโ(๐โsuc ๐ข))) |
394 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ค = (๐โsuc ๐ข) โ (๐บโ๐ค) = (๐บโ(๐โsuc ๐ข))) |
395 | 393, 394 | eqeq12d 2752 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ค = (๐โsuc ๐ข) โ ((๐นโ๐ค) = (๐บโ๐ค) โ (๐นโ(๐โsuc ๐ข)) = (๐บโ(๐โsuc ๐ข)))) |
396 | 392, 395 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ค = (๐โsuc ๐ข) โ ((๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค)) โ (๐ โ (๐โsuc ๐ข) โ (๐นโ(๐โsuc ๐ข)) = (๐บโ(๐โsuc ๐ข))))) |
397 | 396 | rspcv 3577 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โsuc ๐ข) โ ๐ต โ (โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค)) โ (๐ โ (๐โsuc ๐ข) โ (๐นโ(๐โsuc ๐ข)) = (๐บโ(๐โsuc ๐ข))))) |
398 | 202, 378,
391, 397 | syl3c 66 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐นโ(๐โsuc ๐ข)) = (๐บโ(๐โsuc ๐ข))) |
399 | 398 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ ((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) = ((๐ด โo (๐โsuc ๐ข)) ยทo (๐บโ(๐โsuc ๐ข)))) |
400 | 399 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข)) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐บโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข))) |
401 | 376, 400 | eqtr4d 2779 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (๐ปโsuc suc ๐ข) = (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข))) |
402 | 374, 401 | eleq12d 2831 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
)))) โ (((๐ด โo (๐โsuc ๐ข)) ยทo (๐นโ(๐โsuc ๐ข))) +o (๐ปโsuc ๐ข)))) |
403 | 214, 402 | bitr4d 281 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
404 | 403 | biimpd 228 |
. . . . . . . . . . . . . 14
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
405 | 147, 404 | embantd 59 |
. . . . . . . . . . . . 13
โข ((๐ โง (suc ๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข)) โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
406 | 405 | expr 457 |
. . . . . . . . . . . 12
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) โ ๐ข โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
407 | 140, 406 | sylbird 259 |
. . . . . . . . . . 11
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) โ suc ๐ข โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
408 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . 19
โข ((โก๐โ๐) = suc ๐ข โ (๐โ(โก๐โ๐)) = (๐โsuc ๐ข)) |
409 | 408 | sseq2d 3976 |
. . . . . . . . . . . . . . . . . 18
โข ((โก๐โ๐) = suc ๐ข โ (๐ฅ โ (๐โ(โก๐โ๐)) โ ๐ฅ โ (๐โsuc ๐ข))) |
410 | 409 | ifbid 4509 |
. . . . . . . . . . . . . . . . 17
โข ((โก๐โ๐) = suc ๐ข โ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
) = if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
)) |
411 | 410 | mpteq2dv 5207 |
. . . . . . . . . . . . . . . 16
โข ((โก๐โ๐) = suc ๐ข โ (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) |
412 | 411 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
โข ((โก๐โ๐) = suc ๐ข โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
)))) |
413 | | suceq 6383 |
. . . . . . . . . . . . . . . 16
โข ((โก๐โ๐) = suc ๐ข โ suc (โก๐โ๐) = suc suc ๐ข) |
414 | 413 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
โข ((โก๐โ๐) = suc ๐ข โ (๐ปโsuc (โก๐โ๐)) = (๐ปโsuc suc ๐ข)) |
415 | 412, 414 | eleq12d 2831 |
. . . . . . . . . . . . . 14
โข ((โก๐โ๐) = suc ๐ข โ (((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ(โก๐โ๐)), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc (โก๐โ๐)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
416 | 115, 415 | syl5ibcom 244 |
. . . . . . . . . . . . 13
โข (๐ โ ((โก๐โ๐) = suc ๐ข โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
417 | 416 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) = suc ๐ข โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))) |
418 | 417 | a1dd 50 |
. . . . . . . . . . 11
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) = suc ๐ข โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
419 | 407, 418 | jaod 857 |
. . . . . . . . . 10
โข ((๐ โง suc ๐ข โ dom ๐) โ (((โก๐โ๐) โ suc ๐ข โจ (โก๐โ๐) = suc ๐ข) โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
420 | 134, 419 | sylbid 239 |
. . . . . . . . 9
โข ((๐ โง suc ๐ข โ dom ๐) โ ((โก๐โ๐) โ suc ๐ข โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
421 | 420 | expimpd 454 |
. . . . . . . 8
โข (๐ โ ((suc ๐ข โ dom ๐ โง (โก๐โ๐) โ suc ๐ข) โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
422 | 421 | com23 86 |
. . . . . . 7
โข (๐ โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((suc ๐ข โ dom ๐ โง (โก๐โ๐) โ suc ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข)))) |
423 | 422 | a1i 11 |
. . . . . 6
โข (๐ข โ ฯ โ (๐ โ (((๐ข โ dom ๐ โง (โก๐โ๐) โ ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ข)) โ ((suc ๐ข โ dom ๐ โง (โก๐โ๐) โ suc ๐ข) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โsuc ๐ข), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc suc ๐ข))))) |
424 | 82, 94, 106, 127, 423 | finds2 7837 |
. . . . 5
โข (๐ฆ โ ฯ โ (๐ โ ((๐ฆ โ dom ๐ โง (โก๐โ๐) โ ๐ฆ) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โ๐ฆ), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc ๐ฆ)))) |
425 | 70, 424 | vtoclga 3534 |
. . . 4
โข (โช dom ๐ โ ฯ โ (๐ โ ((โช dom
๐ โ dom ๐ โง (โก๐โ๐) โ โช dom
๐) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐)))) |
426 | 57, 425 | mpcom 38 |
. . 3
โข (๐ โ ((โช dom ๐ โ dom ๐ โง (โก๐โ๐) โ โช dom
๐) โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐))) |
427 | 44, 54, 426 | mp2and 697 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) โ (๐ปโsuc โช dom
๐)) |
428 | 155 | feqmptd 6910 |
. . . 4
โข (๐ โ ๐น = (๐ฅ โ ๐ต โฆ (๐นโ๐ฅ))) |
429 | | eqeq2 2748 |
. . . . . 6
โข ((๐นโ๐ฅ) = if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
) โ ((๐นโ๐ฅ) = (๐นโ๐ฅ) โ (๐นโ๐ฅ) = if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) |
430 | | eqeq2 2748 |
. . . . . 6
โข (โ
= if(๐ฅ โ (๐โโช dom ๐), (๐นโ๐ฅ), โ
) โ ((๐นโ๐ฅ) = โ
โ (๐นโ๐ฅ) = if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) |
431 | | eqidd 2737 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต) โง ๐ฅ โ (๐โโช dom
๐)) โ (๐นโ๐ฅ) = (๐นโ๐ฅ)) |
432 | 199 | ffvelcdmi 7034 |
. . . . . . . . . . . . . 14
โข (โช dom ๐ โ dom ๐ โ (๐โโช dom
๐) โ (๐บ supp โ
)) |
433 | 44, 432 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โโช dom
๐) โ (๐บ supp โ
)) |
434 | 197, 433 | sseldd 3945 |
. . . . . . . . . . . 12
โข (๐ โ (๐โโช dom
๐) โ ๐ต) |
435 | | onelon 6342 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง (๐โโช dom ๐) โ ๐ต) โ (๐โโช dom
๐) โ
On) |
436 | 10, 434, 435 | syl2anc 584 |
. . . . . . . . . . 11
โข (๐ โ (๐โโช dom
๐) โ
On) |
437 | 436 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐โโช dom
๐) โ
On) |
438 | | ontri1 6351 |
. . . . . . . . . 10
โข ((๐ฅ โ On โง (๐โโช dom ๐) โ On) โ (๐ฅ โ (๐โโช dom
๐) โ ยฌ (๐โโช dom ๐) โ ๐ฅ)) |
439 | 224, 437,
438 | syl2anc 584 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ โ (๐โโช dom
๐) โ ยฌ (๐โโช dom ๐) โ ๐ฅ)) |
440 | 439 | con2bid 354 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐โโช dom
๐) โ ๐ฅ โ ยฌ ๐ฅ โ (๐โโช dom
๐))) |
441 | | simprl 769 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ๐ฅ โ ๐ต) |
442 | 377 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค))) |
443 | | eloni 6327 |
. . . . . . . . . . . . . . . . . 18
โข ((โก๐โ๐) โ On โ Ord (โก๐โ๐)) |
444 | 129, 443 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ Ord (โก๐โ๐)) |
445 | | orduni 7724 |
. . . . . . . . . . . . . . . . . 18
โข (Ord dom
๐ โ Ord โช dom ๐) |
446 | 36, 445 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข Ord โช dom ๐ |
447 | | ordtri1 6350 |
. . . . . . . . . . . . . . . . 17
โข ((Ord
(โก๐โ๐) โง Ord โช dom
๐) โ ((โก๐โ๐) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐))) |
448 | 444, 446,
447 | sylancl 586 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โก๐โ๐) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐))) |
449 | 54, 448 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ ยฌ โช dom ๐ โ (โก๐โ๐)) |
450 | | isorel 7271 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง (โช dom ๐ โ dom ๐ โง (โก๐โ๐) โ dom ๐)) โ (โช dom
๐ E (โก๐โ๐) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐)))) |
451 | 46, 44, 52, 450 | syl12anc 835 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โช dom ๐ E (โก๐โ๐) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐)))) |
452 | | fvex 6855 |
. . . . . . . . . . . . . . . . . 18
โข (โก๐โ๐) โ V |
453 | 452 | epeli 5539 |
. . . . . . . . . . . . . . . . 17
โข (โช dom ๐ E (โก๐โ๐) โ โช dom
๐ โ (โก๐โ๐)) |
454 | | fvex 6855 |
. . . . . . . . . . . . . . . . . 18
โข (๐โ(โก๐โ๐)) โ V |
455 | 454 | epeli 5539 |
. . . . . . . . . . . . . . . . 17
โข ((๐โโช dom ๐) E (๐โ(โก๐โ๐)) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐))) |
456 | 451, 453,
455 | 3bitr3g 312 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โช dom ๐ โ (โก๐โ๐) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐)))) |
457 | 108 | eleq2d 2823 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐โโช dom
๐) โ (๐โ(โก๐โ๐)) โ (๐โโช dom
๐) โ ๐)) |
458 | 456, 457 | bitrd 278 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โช dom ๐ โ (โก๐โ๐) โ (๐โโช dom
๐) โ ๐)) |
459 | 449, 458 | mtbid 323 |
. . . . . . . . . . . . . 14
โข (๐ โ ยฌ (๐โโช dom
๐) โ ๐) |
460 | | onelon 6342 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ On โง ๐ โ ๐ต) โ ๐ โ On) |
461 | 10, 161, 460 | syl2anc 584 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ On) |
462 | | ontri1 6351 |
. . . . . . . . . . . . . . 15
โข ((๐ โ On โง (๐โโช dom ๐) โ On) โ (๐ โ (๐โโช dom
๐) โ ยฌ (๐โโช dom ๐) โ ๐)) |
463 | 461, 436,
462 | syl2anc 584 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ (๐โโช dom
๐) โ ยฌ (๐โโช dom ๐) โ ๐)) |
464 | 459, 463 | mpbird 256 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐โโช dom
๐)) |
465 | 464 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ๐ โ (๐โโช dom
๐)) |
466 | | simprr 771 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ (๐โโช dom
๐) โ ๐ฅ) |
467 | 224 | adantrr 715 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ๐ฅ โ On) |
468 | | ontr2 6364 |
. . . . . . . . . . . . 13
โข ((๐ โ On โง ๐ฅ โ On) โ ((๐ โ (๐โโช dom
๐) โง (๐โโช dom
๐) โ ๐ฅ) โ ๐ โ ๐ฅ)) |
469 | 461, 467,
468 | syl2an2r 683 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ((๐ โ (๐โโช dom
๐) โง (๐โโช dom
๐) โ ๐ฅ) โ ๐ โ ๐ฅ)) |
470 | 465, 466,
469 | mp2and 697 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ๐ โ ๐ฅ) |
471 | | eleq2 2826 |
. . . . . . . . . . . . 13
โข (๐ค = ๐ฅ โ (๐ โ ๐ค โ ๐ โ ๐ฅ)) |
472 | | fveq2 6842 |
. . . . . . . . . . . . . 14
โข (๐ค = ๐ฅ โ (๐นโ๐ค) = (๐นโ๐ฅ)) |
473 | | fveq2 6842 |
. . . . . . . . . . . . . 14
โข (๐ค = ๐ฅ โ (๐บโ๐ค) = (๐บโ๐ฅ)) |
474 | 472, 473 | eqeq12d 2752 |
. . . . . . . . . . . . 13
โข (๐ค = ๐ฅ โ ((๐นโ๐ค) = (๐บโ๐ค) โ (๐นโ๐ฅ) = (๐บโ๐ฅ))) |
475 | 471, 474 | imbi12d 344 |
. . . . . . . . . . . 12
โข (๐ค = ๐ฅ โ ((๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค)) โ (๐ โ ๐ฅ โ (๐นโ๐ฅ) = (๐บโ๐ฅ)))) |
476 | 475 | rspcv 3577 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ต โ (โ๐ค โ ๐ต (๐ โ ๐ค โ (๐นโ๐ค) = (๐บโ๐ค)) โ (๐ โ ๐ฅ โ (๐นโ๐ฅ) = (๐บโ๐ฅ)))) |
477 | 441, 442,
470, 476 | syl3c 66 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ (๐นโ๐ฅ) = (๐บโ๐ฅ)) |
478 | 466 | adantr 481 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (๐โโช dom
๐) โ ๐ฅ) |
479 | 46 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ ๐ Isom E , E (dom ๐, (๐บ supp โ
))) |
480 | 44 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ โช dom ๐ โ dom ๐) |
481 | 51 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ โก๐:(๐บ supp โ
)โถdom ๐) |
482 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . . . 18
โข ((โก๐:(๐บ supp โ
)โถdom ๐ โง ๐ฅ โ (๐บ supp โ
)) โ (โก๐โ๐ฅ) โ dom ๐) |
483 | 481, 482 | sylancom 588 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โก๐โ๐ฅ) โ dom ๐) |
484 | | isorel 7271 |
. . . . . . . . . . . . . . . . 17
โข ((๐ Isom E , E (dom ๐, (๐บ supp โ
)) โง (โช dom ๐ โ dom ๐ โง (โก๐โ๐ฅ) โ dom ๐)) โ (โช dom
๐ E (โก๐โ๐ฅ) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐ฅ)))) |
485 | 479, 480,
483, 484 | syl12anc 835 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โช dom ๐ E (โก๐โ๐ฅ) โ (๐โโช dom
๐) E (๐โ(โก๐โ๐ฅ)))) |
486 | 269 | epeli 5539 |
. . . . . . . . . . . . . . . 16
โข (โช dom ๐ E (โก๐โ๐ฅ) โ โช dom
๐ โ (โก๐โ๐ฅ)) |
487 | 271 | epeli 5539 |
. . . . . . . . . . . . . . . 16
โข ((๐โโช dom ๐) E (๐โ(โก๐โ๐ฅ)) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐ฅ))) |
488 | 485, 486,
487 | 3bitr3g 312 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โช dom ๐ โ (โก๐โ๐ฅ) โ (๐โโช dom
๐) โ (๐โ(โก๐โ๐ฅ)))) |
489 | 48 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ ๐:dom ๐โ1-1-ontoโ(๐บ supp โ
)) |
490 | 489, 261 | sylancom 588 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (๐โ(โก๐โ๐ฅ)) = ๐ฅ) |
491 | 490 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ ((๐โโช dom
๐) โ (๐โ(โก๐โ๐ฅ)) โ (๐โโช dom
๐) โ ๐ฅ)) |
492 | 488, 491 | bitrd 278 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โช dom ๐ โ (โก๐โ๐ฅ) โ (๐โโช dom
๐) โ ๐ฅ)) |
493 | 478, 492 | mpbird 256 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ โช dom ๐ โ (โก๐โ๐ฅ)) |
494 | | elssuni 4898 |
. . . . . . . . . . . . . . 15
โข ((โก๐โ๐ฅ) โ dom ๐ โ (โก๐โ๐ฅ) โ โช dom
๐) |
495 | 483, 494 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โก๐โ๐ฅ) โ โช dom
๐) |
496 | 36, 483, 275 | sylancr 587 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ (โก๐โ๐ฅ) โ On) |
497 | 496, 277 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ Ord (โก๐โ๐ฅ)) |
498 | | ordtri1 6350 |
. . . . . . . . . . . . . . 15
โข ((Ord
(โก๐โ๐ฅ) โง Ord โช dom
๐) โ ((โก๐โ๐ฅ) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐ฅ))) |
499 | 497, 446,
498 | sylancl 586 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ ((โก๐โ๐ฅ) โ โช dom
๐ โ ยฌ โช dom ๐ โ (โก๐โ๐ฅ))) |
500 | 495, 499 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โง ๐ฅ โ (๐บ supp โ
)) โ ยฌ โช dom ๐ โ (โก๐โ๐ฅ)) |
501 | 493, 500 | pm2.65da 815 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ยฌ ๐ฅ โ (๐บ supp โ
)) |
502 | 441, 501 | eldifd 3921 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ ๐ฅ โ (๐ต โ (๐บ supp โ
))) |
503 | | ssidd 3967 |
. . . . . . . . . . . 12
โข (๐ โ (๐บ supp โ
) โ (๐บ supp โ
)) |
504 | 159, 503,
10, 176 | suppssr 8127 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ต โ (๐บ supp โ
))) โ (๐บโ๐ฅ) = โ
) |
505 | 502, 504 | syldan 591 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ (๐บโ๐ฅ) = โ
) |
506 | 477, 505 | eqtrd 2776 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ต โง (๐โโช dom
๐) โ ๐ฅ)) โ (๐นโ๐ฅ) = โ
) |
507 | 506 | expr 457 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐โโช dom
๐) โ ๐ฅ โ (๐นโ๐ฅ) = โ
)) |
508 | 440, 507 | sylbird 259 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ต) โ (ยฌ ๐ฅ โ (๐โโช dom
๐) โ (๐นโ๐ฅ) = โ
)) |
509 | 508 | imp 407 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต) โง ยฌ ๐ฅ โ (๐โโช dom
๐)) โ (๐นโ๐ฅ) = โ
) |
510 | 429, 430,
431, 509 | ifbothda 4524 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐นโ๐ฅ) = if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
)) |
511 | 510 | mpteq2dva 5205 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ต โฆ (๐นโ๐ฅ)) = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) |
512 | 428, 511 | eqtrd 2776 |
. . 3
โข (๐ โ ๐น = (๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
))) |
513 | 512 | fveq2d 6846 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = ((๐ด CNF ๐ต)โ(๐ฅ โ ๐ต โฆ if(๐ฅ โ (๐โโช dom
๐), (๐นโ๐ฅ), โ
)))) |
514 | 8, 9, 10, 2, 13, 113 | cantnfval 9604 |
. . 3
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) = (๐ปโdom ๐)) |
515 | 43 | fveq2d 6846 |
. . 3
โข (๐ โ (๐ปโdom ๐) = (๐ปโsuc โช dom
๐)) |
516 | 514, 515 | eqtrd 2776 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐บ) = (๐ปโsuc โช dom
๐)) |
517 | 427, 513,
516 | 3eltr4d 2852 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) โ ((๐ด CNF ๐ต)โ๐บ)) |