Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
โข ๐ = dom ( ๐ด CNF ๐ต ) |
2 |
|
cantnfs.a |
โข ( ๐ โ ๐ด โ On ) |
3 |
|
cantnfs.b |
โข ( ๐ โ ๐ต โ On ) |
4 |
|
cantnfp1.g |
โข ( ๐ โ ๐บ โ ๐ ) |
5 |
|
cantnfp1.x |
โข ( ๐ โ ๐ โ ๐ต ) |
6 |
|
cantnfp1.y |
โข ( ๐ โ ๐ โ ๐ด ) |
7 |
|
cantnfp1.s |
โข ( ๐ โ ( ๐บ supp โ
) โ ๐ ) |
8 |
|
cantnfp1.f |
โข ๐น = ( ๐ก โ ๐ต โฆ if ( ๐ก = ๐ , ๐ , ( ๐บ โ ๐ก ) ) ) |
9 |
|
cantnfp1.e |
โข ( ๐ โ โ
โ ๐ ) |
10 |
|
cantnfp1.o |
โข ๐ = OrdIso ( E , ( ๐น supp โ
) ) |
11 |
|
cantnfp1.h |
โข ๐ป = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( ๐ โ ๐ ) ) ยทo ( ๐น โ ( ๐ โ ๐ ) ) ) +o ๐ง ) ) , โ
) |
12 |
|
cantnfp1.k |
โข ๐พ = OrdIso ( E , ( ๐บ supp โ
) ) |
13 |
|
cantnfp1.m |
โข ๐ = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( ๐พ โ ๐ ) ) ยทo ( ๐บ โ ( ๐พ โ ๐ ) ) ) +o ๐ง ) ) , โ
) |
14 |
1 2 3 4 5 6 7 8
|
cantnfp1lem1 |
โข ( ๐ โ ๐น โ ๐ ) |
15 |
1 2 3 10 14 11
|
cantnfval |
โข ( ๐ โ ( ( ๐ด CNF ๐ต ) โ ๐น ) = ( ๐ป โ dom ๐ ) ) |
16 |
1 2 3 4 5 6 7 8 9 10
|
cantnfp1lem2 |
โข ( ๐ โ dom ๐ = suc โช dom ๐ ) |
17 |
16
|
fveq2d |
โข ( ๐ โ ( ๐ป โ dom ๐ ) = ( ๐ป โ suc โช dom ๐ ) ) |
18 |
1 2 3 10 14
|
cantnfcl |
โข ( ๐ โ ( E We ( ๐น supp โ
) โง dom ๐ โ ฯ ) ) |
19 |
18
|
simprd |
โข ( ๐ โ dom ๐ โ ฯ ) |
20 |
16 19
|
eqeltrrd |
โข ( ๐ โ suc โช dom ๐ โ ฯ ) |
21 |
|
peano2b |
โข ( โช dom ๐ โ ฯ โ suc โช dom ๐ โ ฯ ) |
22 |
20 21
|
sylibr |
โข ( ๐ โ โช dom ๐ โ ฯ ) |
23 |
1 2 3 10 14 11
|
cantnfsuc |
โข ( ( ๐ โง โช dom ๐ โ ฯ ) โ ( ๐ป โ suc โช dom ๐ ) = ( ( ( ๐ด โo ( ๐ โ โช dom ๐ ) ) ยทo ( ๐น โ ( ๐ โ โช dom ๐ ) ) ) +o ( ๐ป โ โช dom ๐ ) ) ) |
24 |
22 23
|
mpdan |
โข ( ๐ โ ( ๐ป โ suc โช dom ๐ ) = ( ( ( ๐ด โo ( ๐ โ โช dom ๐ ) ) ยทo ( ๐น โ ( ๐ โ โช dom ๐ ) ) ) +o ( ๐ป โ โช dom ๐ ) ) ) |
25 |
|
ovexd |
โข ( ๐ โ ( ๐น supp โ
) โ V ) |
26 |
18
|
simpld |
โข ( ๐ โ E We ( ๐น supp โ
) ) |
27 |
10
|
oiiso |
โข ( ( ( ๐น supp โ
) โ V โง E We ( ๐น supp โ
) ) โ ๐ Isom E , E ( dom ๐ , ( ๐น supp โ
) ) ) |
28 |
25 26 27
|
syl2anc |
โข ( ๐ โ ๐ Isom E , E ( dom ๐ , ( ๐น supp โ
) ) ) |
29 |
|
isof1o |
โข ( ๐ Isom E , E ( dom ๐ , ( ๐น supp โ
) ) โ ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) ) |
30 |
28 29
|
syl |
โข ( ๐ โ ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) ) |
31 |
|
f1ocnv |
โข ( ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) โ โก ๐ : ( ๐น supp โ
) โ1-1-ontoโ dom ๐ ) |
32 |
|
f1of |
โข ( โก ๐ : ( ๐น supp โ
) โ1-1-ontoโ dom ๐ โ โก ๐ : ( ๐น supp โ
) โถ dom ๐ ) |
33 |
30 31 32
|
3syl |
โข ( ๐ โ โก ๐ : ( ๐น supp โ
) โถ dom ๐ ) |
34 |
|
iftrue |
โข ( ๐ก = ๐ โ if ( ๐ก = ๐ , ๐ , ( ๐บ โ ๐ก ) ) = ๐ ) |
35 |
8 34 5 6
|
fvmptd3 |
โข ( ๐ โ ( ๐น โ ๐ ) = ๐ ) |
36 |
9
|
ne0d |
โข ( ๐ โ ๐ โ โ
) |
37 |
35 36
|
eqnetrd |
โข ( ๐ โ ( ๐น โ ๐ ) โ โ
) |
38 |
6
|
adantr |
โข ( ( ๐ โง ๐ก โ ๐ต ) โ ๐ โ ๐ด ) |
39 |
1 2 3
|
cantnfs |
โข ( ๐ โ ( ๐บ โ ๐ โ ( ๐บ : ๐ต โถ ๐ด โง ๐บ finSupp โ
) ) ) |
40 |
4 39
|
mpbid |
โข ( ๐ โ ( ๐บ : ๐ต โถ ๐ด โง ๐บ finSupp โ
) ) |
41 |
40
|
simpld |
โข ( ๐ โ ๐บ : ๐ต โถ ๐ด ) |
42 |
41
|
ffvelrnda |
โข ( ( ๐ โง ๐ก โ ๐ต ) โ ( ๐บ โ ๐ก ) โ ๐ด ) |
43 |
38 42
|
ifcld |
โข ( ( ๐ โง ๐ก โ ๐ต ) โ if ( ๐ก = ๐ , ๐ , ( ๐บ โ ๐ก ) ) โ ๐ด ) |
44 |
43 8
|
fmptd |
โข ( ๐ โ ๐น : ๐ต โถ ๐ด ) |
45 |
44
|
ffnd |
โข ( ๐ โ ๐น Fn ๐ต ) |
46 |
|
0ex |
โข โ
โ V |
47 |
46
|
a1i |
โข ( ๐ โ โ
โ V ) |
48 |
|
elsuppfn |
โข ( ( ๐น Fn ๐ต โง ๐ต โ On โง โ
โ V ) โ ( ๐ โ ( ๐น supp โ
) โ ( ๐ โ ๐ต โง ( ๐น โ ๐ ) โ โ
) ) ) |
49 |
45 3 47 48
|
syl3anc |
โข ( ๐ โ ( ๐ โ ( ๐น supp โ
) โ ( ๐ โ ๐ต โง ( ๐น โ ๐ ) โ โ
) ) ) |
50 |
5 37 49
|
mpbir2and |
โข ( ๐ โ ๐ โ ( ๐น supp โ
) ) |
51 |
33 50
|
ffvelrnd |
โข ( ๐ โ ( โก ๐ โ ๐ ) โ dom ๐ ) |
52 |
|
elssuni |
โข ( ( โก ๐ โ ๐ ) โ dom ๐ โ ( โก ๐ โ ๐ ) โ โช dom ๐ ) |
53 |
51 52
|
syl |
โข ( ๐ โ ( โก ๐ โ ๐ ) โ โช dom ๐ ) |
54 |
10
|
oicl |
โข Ord dom ๐ |
55 |
|
ordelon |
โข ( ( Ord dom ๐ โง ( โก ๐ โ ๐ ) โ dom ๐ ) โ ( โก ๐ โ ๐ ) โ On ) |
56 |
54 51 55
|
sylancr |
โข ( ๐ โ ( โก ๐ โ ๐ ) โ On ) |
57 |
|
nnon |
โข ( โช dom ๐ โ ฯ โ โช dom ๐ โ On ) |
58 |
22 57
|
syl |
โข ( ๐ โ โช dom ๐ โ On ) |
59 |
|
ontri1 |
โข ( ( ( โก ๐ โ ๐ ) โ On โง โช dom ๐ โ On ) โ ( ( โก ๐ โ ๐ ) โ โช dom ๐ โ ยฌ โช dom ๐ โ ( โก ๐ โ ๐ ) ) ) |
60 |
56 58 59
|
syl2anc |
โข ( ๐ โ ( ( โก ๐ โ ๐ ) โ โช dom ๐ โ ยฌ โช dom ๐ โ ( โก ๐ โ ๐ ) ) ) |
61 |
53 60
|
mpbid |
โข ( ๐ โ ยฌ โช dom ๐ โ ( โก ๐ โ ๐ ) ) |
62 |
|
sucidg |
โข ( โช dom ๐ โ ฯ โ โช dom ๐ โ suc โช dom ๐ ) |
63 |
22 62
|
syl |
โข ( ๐ โ โช dom ๐ โ suc โช dom ๐ ) |
64 |
63 16
|
eleqtrrd |
โข ( ๐ โ โช dom ๐ โ dom ๐ ) |
65 |
|
isorel |
โข ( ( ๐ Isom E , E ( dom ๐ , ( ๐น supp โ
) ) โง ( โช dom ๐ โ dom ๐ โง ( โก ๐ โ ๐ ) โ dom ๐ ) ) โ ( โช dom ๐ E ( โก ๐ โ ๐ ) โ ( ๐ โ โช dom ๐ ) E ( ๐ โ ( โก ๐ โ ๐ ) ) ) ) |
66 |
28 64 51 65
|
syl12anc |
โข ( ๐ โ ( โช dom ๐ E ( โก ๐ โ ๐ ) โ ( ๐ โ โช dom ๐ ) E ( ๐ โ ( โก ๐ โ ๐ ) ) ) ) |
67 |
|
fvex |
โข ( โก ๐ โ ๐ ) โ V |
68 |
67
|
epeli |
โข ( โช dom ๐ E ( โก ๐ โ ๐ ) โ โช dom ๐ โ ( โก ๐ โ ๐ ) ) |
69 |
|
fvex |
โข ( ๐ โ ( โก ๐ โ ๐ ) ) โ V |
70 |
69
|
epeli |
โข ( ( ๐ โ โช dom ๐ ) E ( ๐ โ ( โก ๐ โ ๐ ) ) โ ( ๐ โ โช dom ๐ ) โ ( ๐ โ ( โก ๐ โ ๐ ) ) ) |
71 |
66 68 70
|
3bitr3g |
โข ( ๐ โ ( โช dom ๐ โ ( โก ๐ โ ๐ ) โ ( ๐ โ โช dom ๐ ) โ ( ๐ โ ( โก ๐ โ ๐ ) ) ) ) |
72 |
|
f1ocnvfv2 |
โข ( ( ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) โง ๐ โ ( ๐น supp โ
) ) โ ( ๐ โ ( โก ๐ โ ๐ ) ) = ๐ ) |
73 |
30 50 72
|
syl2anc |
โข ( ๐ โ ( ๐ โ ( โก ๐ โ ๐ ) ) = ๐ ) |
74 |
73
|
eleq2d |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ ( ๐ โ ( โก ๐ โ ๐ ) ) โ ( ๐ โ โช dom ๐ ) โ ๐ ) ) |
75 |
71 74
|
bitrd |
โข ( ๐ โ ( โช dom ๐ โ ( โก ๐ โ ๐ ) โ ( ๐ โ โช dom ๐ ) โ ๐ ) ) |
76 |
61 75
|
mtbid |
โข ( ๐ โ ยฌ ( ๐ โ โช dom ๐ ) โ ๐ ) |
77 |
7
|
sseld |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ ( ๐บ supp โ
) โ ( ๐ โ โช dom ๐ ) โ ๐ ) ) |
78 |
|
suppssdm |
โข ( ๐น supp โ
) โ dom ๐น |
79 |
78 44
|
fssdm |
โข ( ๐ โ ( ๐น supp โ
) โ ๐ต ) |
80 |
|
onss |
โข ( ๐ต โ On โ ๐ต โ On ) |
81 |
3 80
|
syl |
โข ( ๐ โ ๐ต โ On ) |
82 |
79 81
|
sstrd |
โข ( ๐ โ ( ๐น supp โ
) โ On ) |
83 |
10
|
oif |
โข ๐ : dom ๐ โถ ( ๐น supp โ
) |
84 |
83
|
ffvelrni |
โข ( โช dom ๐ โ dom ๐ โ ( ๐ โ โช dom ๐ ) โ ( ๐น supp โ
) ) |
85 |
64 84
|
syl |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) โ ( ๐น supp โ
) ) |
86 |
82 85
|
sseldd |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) โ On ) |
87 |
|
eloni |
โข ( ( ๐ โ โช dom ๐ ) โ On โ Ord ( ๐ โ โช dom ๐ ) ) |
88 |
86 87
|
syl |
โข ( ๐ โ Ord ( ๐ โ โช dom ๐ ) ) |
89 |
|
ordn2lp |
โข ( Ord ( ๐ โ โช dom ๐ ) โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โง ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
90 |
88 89
|
syl |
โข ( ๐ โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โง ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
91 |
|
imnan |
โข ( ( ( ๐ โ โช dom ๐ ) โ ๐ โ ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โง ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
92 |
90 91
|
sylibr |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ ๐ โ ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
93 |
77 92
|
syld |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ ( ๐บ supp โ
) โ ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
94 |
|
onelon |
โข ( ( ๐ต โ On โง ๐ โ ๐ต ) โ ๐ โ On ) |
95 |
3 5 94
|
syl2anc |
โข ( ๐ โ ๐ โ On ) |
96 |
|
eloni |
โข ( ๐ โ On โ Ord ๐ ) |
97 |
95 96
|
syl |
โข ( ๐ โ Ord ๐ ) |
98 |
|
ordirr |
โข ( Ord ๐ โ ยฌ ๐ โ ๐ ) |
99 |
97 98
|
syl |
โข ( ๐ โ ยฌ ๐ โ ๐ ) |
100 |
|
elsni |
โข ( ( ๐ โ โช dom ๐ ) โ { ๐ } โ ( ๐ โ โช dom ๐ ) = ๐ ) |
101 |
100
|
eleq2d |
โข ( ( ๐ โ โช dom ๐ ) โ { ๐ } โ ( ๐ โ ( ๐ โ โช dom ๐ ) โ ๐ โ ๐ ) ) |
102 |
101
|
notbid |
โข ( ( ๐ โ โช dom ๐ ) โ { ๐ } โ ( ยฌ ๐ โ ( ๐ โ โช dom ๐ ) โ ยฌ ๐ โ ๐ ) ) |
103 |
99 102
|
syl5ibrcom |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ { ๐ } โ ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
104 |
|
eqeq1 |
โข ( ๐ก = ๐ โ ( ๐ก = ๐ โ ๐ = ๐ ) ) |
105 |
|
fveq2 |
โข ( ๐ก = ๐ โ ( ๐บ โ ๐ก ) = ( ๐บ โ ๐ ) ) |
106 |
104 105
|
ifbieq2d |
โข ( ๐ก = ๐ โ if ( ๐ก = ๐ , ๐ , ( ๐บ โ ๐ก ) ) = if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) ) |
107 |
|
eldifi |
โข ( ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) โ ๐ โ ๐ต ) |
108 |
107
|
adantl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ๐ โ ๐ต ) |
109 |
6
|
adantr |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ๐ โ ๐ด ) |
110 |
|
fvex |
โข ( ๐บ โ ๐ ) โ V |
111 |
|
ifexg |
โข ( ( ๐ โ ๐ด โง ( ๐บ โ ๐ ) โ V ) โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) โ V ) |
112 |
109 110 111
|
sylancl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) โ V ) |
113 |
8 106 108 112
|
fvmptd3 |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ( ๐น โ ๐ ) = if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) ) |
114 |
|
eldifn |
โข ( ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) โ ยฌ ๐ โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
115 |
114
|
adantl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ยฌ ๐ โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
116 |
|
velsn |
โข ( ๐ โ { ๐ } โ ๐ = ๐ ) |
117 |
|
elun2 |
โข ( ๐ โ { ๐ } โ ๐ โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
118 |
116 117
|
sylbir |
โข ( ๐ = ๐ โ ๐ โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
119 |
115 118
|
nsyl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ยฌ ๐ = ๐ ) |
120 |
119
|
iffalsed |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) = ( ๐บ โ ๐ ) ) |
121 |
|
ssun1 |
โข ( ๐บ supp โ
) โ ( ( ๐บ supp โ
) โช { ๐ } ) |
122 |
|
sscon |
โข ( ( ๐บ supp โ
) โ ( ( ๐บ supp โ
) โช { ๐ } ) โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) โ ( ๐ต โ ( ๐บ supp โ
) ) ) |
123 |
121 122
|
ax-mp |
โข ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) โ ( ๐ต โ ( ๐บ supp โ
) ) |
124 |
123
|
sseli |
โข ( ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) โ ๐ โ ( ๐ต โ ( ๐บ supp โ
) ) ) |
125 |
|
ssidd |
โข ( ๐ โ ( ๐บ supp โ
) โ ( ๐บ supp โ
) ) |
126 |
41 125 3 9
|
suppssr |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐บ supp โ
) ) ) โ ( ๐บ โ ๐ ) = โ
) |
127 |
124 126
|
sylan2 |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ( ๐บ โ ๐ ) = โ
) |
128 |
113 120 127
|
3eqtrd |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ( ๐บ supp โ
) โช { ๐ } ) ) ) โ ( ๐น โ ๐ ) = โ
) |
129 |
44 128
|
suppss |
โข ( ๐ โ ( ๐น supp โ
) โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
130 |
129 85
|
sseldd |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) โ ( ( ๐บ supp โ
) โช { ๐ } ) ) |
131 |
|
elun |
โข ( ( ๐ โ โช dom ๐ ) โ ( ( ๐บ supp โ
) โช { ๐ } ) โ ( ( ๐ โ โช dom ๐ ) โ ( ๐บ supp โ
) โจ ( ๐ โ โช dom ๐ ) โ { ๐ } ) ) |
132 |
130 131
|
sylib |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) โ ( ๐บ supp โ
) โจ ( ๐ โ โช dom ๐ ) โ { ๐ } ) ) |
133 |
93 103 132
|
mpjaod |
โข ( ๐ โ ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) |
134 |
|
ioran |
โข ( ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โจ ๐ โ ( ๐ โ โช dom ๐ ) ) โ ( ยฌ ( ๐ โ โช dom ๐ ) โ ๐ โง ยฌ ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
135 |
76 133 134
|
sylanbrc |
โข ( ๐ โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โจ ๐ โ ( ๐ โ โช dom ๐ ) ) ) |
136 |
|
ordtri3 |
โข ( ( Ord ( ๐ โ โช dom ๐ ) โง Ord ๐ ) โ ( ( ๐ โ โช dom ๐ ) = ๐ โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โจ ๐ โ ( ๐ โ โช dom ๐ ) ) ) ) |
137 |
88 97 136
|
syl2anc |
โข ( ๐ โ ( ( ๐ โ โช dom ๐ ) = ๐ โ ยฌ ( ( ๐ โ โช dom ๐ ) โ ๐ โจ ๐ โ ( ๐ โ โช dom ๐ ) ) ) ) |
138 |
135 137
|
mpbird |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) = ๐ ) |
139 |
138
|
oveq2d |
โข ( ๐ โ ( ๐ด โo ( ๐ โ โช dom ๐ ) ) = ( ๐ด โo ๐ ) ) |
140 |
138
|
fveq2d |
โข ( ๐ โ ( ๐น โ ( ๐ โ โช dom ๐ ) ) = ( ๐น โ ๐ ) ) |
141 |
140 35
|
eqtrd |
โข ( ๐ โ ( ๐น โ ( ๐ โ โช dom ๐ ) ) = ๐ ) |
142 |
139 141
|
oveq12d |
โข ( ๐ โ ( ( ๐ด โo ( ๐ โ โช dom ๐ ) ) ยทo ( ๐น โ ( ๐ โ โช dom ๐ ) ) ) = ( ( ๐ด โo ๐ ) ยทo ๐ ) ) |
143 |
|
nnord |
โข ( โช dom ๐ โ ฯ โ Ord โช dom ๐ ) |
144 |
22 143
|
syl |
โข ( ๐ โ Ord โช dom ๐ ) |
145 |
|
sssucid |
โข โช dom ๐ โ suc โช dom ๐ |
146 |
145 16
|
sseqtrrid |
โข ( ๐ โ โช dom ๐ โ dom ๐ ) |
147 |
|
f1ofo |
โข ( ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) โ ๐ : dom ๐ โontoโ ( ๐น supp โ
) ) |
148 |
30 147
|
syl |
โข ( ๐ โ ๐ : dom ๐ โontoโ ( ๐น supp โ
) ) |
149 |
|
foima |
โข ( ๐ : dom ๐ โontoโ ( ๐น supp โ
) โ ( ๐ โ dom ๐ ) = ( ๐น supp โ
) ) |
150 |
148 149
|
syl |
โข ( ๐ โ ( ๐ โ dom ๐ ) = ( ๐น supp โ
) ) |
151 |
|
ffn |
โข ( ๐ : dom ๐ โถ ( ๐น supp โ
) โ ๐ Fn dom ๐ ) |
152 |
83 151
|
ax-mp |
โข ๐ Fn dom ๐ |
153 |
|
fnsnfv |
โข ( ( ๐ Fn dom ๐ โง โช dom ๐ โ dom ๐ ) โ { ( ๐ โ โช dom ๐ ) } = ( ๐ โ { โช dom ๐ } ) ) |
154 |
152 64 153
|
sylancr |
โข ( ๐ โ { ( ๐ โ โช dom ๐ ) } = ( ๐ โ { โช dom ๐ } ) ) |
155 |
138
|
sneqd |
โข ( ๐ โ { ( ๐ โ โช dom ๐ ) } = { ๐ } ) |
156 |
154 155
|
eqtr3d |
โข ( ๐ โ ( ๐ โ { โช dom ๐ } ) = { ๐ } ) |
157 |
150 156
|
difeq12d |
โข ( ๐ โ ( ( ๐ โ dom ๐ ) โ ( ๐ โ { โช dom ๐ } ) ) = ( ( ๐น supp โ
) โ { ๐ } ) ) |
158 |
|
ordirr |
โข ( Ord โช dom ๐ โ ยฌ โช dom ๐ โ โช dom ๐ ) |
159 |
144 158
|
syl |
โข ( ๐ โ ยฌ โช dom ๐ โ โช dom ๐ ) |
160 |
|
disjsn |
โข ( ( โช dom ๐ โฉ { โช dom ๐ } ) = โ
โ ยฌ โช dom ๐ โ โช dom ๐ ) |
161 |
159 160
|
sylibr |
โข ( ๐ โ ( โช dom ๐ โฉ { โช dom ๐ } ) = โ
) |
162 |
|
disj3 |
โข ( ( โช dom ๐ โฉ { โช dom ๐ } ) = โ
โ โช dom ๐ = ( โช dom ๐ โ { โช dom ๐ } ) ) |
163 |
161 162
|
sylib |
โข ( ๐ โ โช dom ๐ = ( โช dom ๐ โ { โช dom ๐ } ) ) |
164 |
|
difun2 |
โข ( ( โช dom ๐ โช { โช dom ๐ } ) โ { โช dom ๐ } ) = ( โช dom ๐ โ { โช dom ๐ } ) |
165 |
163 164
|
eqtr4di |
โข ( ๐ โ โช dom ๐ = ( ( โช dom ๐ โช { โช dom ๐ } ) โ { โช dom ๐ } ) ) |
166 |
|
df-suc |
โข suc โช dom ๐ = ( โช dom ๐ โช { โช dom ๐ } ) |
167 |
16 166
|
eqtrdi |
โข ( ๐ โ dom ๐ = ( โช dom ๐ โช { โช dom ๐ } ) ) |
168 |
167
|
difeq1d |
โข ( ๐ โ ( dom ๐ โ { โช dom ๐ } ) = ( ( โช dom ๐ โช { โช dom ๐ } ) โ { โช dom ๐ } ) ) |
169 |
165 168
|
eqtr4d |
โข ( ๐ โ โช dom ๐ = ( dom ๐ โ { โช dom ๐ } ) ) |
170 |
169
|
imaeq2d |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) = ( ๐ โ ( dom ๐ โ { โช dom ๐ } ) ) ) |
171 |
|
dff1o3 |
โข ( ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) โ ( ๐ : dom ๐ โontoโ ( ๐น supp โ
) โง Fun โก ๐ ) ) |
172 |
171
|
simprbi |
โข ( ๐ : dom ๐ โ1-1-ontoโ ( ๐น supp โ
) โ Fun โก ๐ ) |
173 |
|
imadif |
โข ( Fun โก ๐ โ ( ๐ โ ( dom ๐ โ { โช dom ๐ } ) ) = ( ( ๐ โ dom ๐ ) โ ( ๐ โ { โช dom ๐ } ) ) ) |
174 |
30 172 173
|
3syl |
โข ( ๐ โ ( ๐ โ ( dom ๐ โ { โช dom ๐ } ) ) = ( ( ๐ โ dom ๐ ) โ ( ๐ โ { โช dom ๐ } ) ) ) |
175 |
170 174
|
eqtrd |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) = ( ( ๐ โ dom ๐ ) โ ( ๐ โ { โช dom ๐ } ) ) ) |
176 |
7 99
|
ssneldd |
โข ( ๐ โ ยฌ ๐ โ ( ๐บ supp โ
) ) |
177 |
|
disjsn |
โข ( ( ( ๐บ supp โ
) โฉ { ๐ } ) = โ
โ ยฌ ๐ โ ( ๐บ supp โ
) ) |
178 |
176 177
|
sylibr |
โข ( ๐ โ ( ( ๐บ supp โ
) โฉ { ๐ } ) = โ
) |
179 |
|
fvex |
โข ( ๐บ โ ๐ ) โ V |
180 |
|
dif1o |
โข ( ( ๐บ โ ๐ ) โ ( V โ 1o ) โ ( ( ๐บ โ ๐ ) โ V โง ( ๐บ โ ๐ ) โ โ
) ) |
181 |
179 180
|
mpbiran |
โข ( ( ๐บ โ ๐ ) โ ( V โ 1o ) โ ( ๐บ โ ๐ ) โ โ
) |
182 |
41
|
ffnd |
โข ( ๐ โ ๐บ Fn ๐ต ) |
183 |
|
elsuppfn |
โข ( ( ๐บ Fn ๐ต โง ๐ต โ On โง โ
โ V ) โ ( ๐ โ ( ๐บ supp โ
) โ ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ โ
) ) ) |
184 |
182 3 47 183
|
syl3anc |
โข ( ๐ โ ( ๐ โ ( ๐บ supp โ
) โ ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ โ
) ) ) |
185 |
181
|
a1i |
โข ( ๐ โ ( ( ๐บ โ ๐ ) โ ( V โ 1o ) โ ( ๐บ โ ๐ ) โ โ
) ) |
186 |
185
|
bicomd |
โข ( ๐ โ ( ( ๐บ โ ๐ ) โ โ
โ ( ๐บ โ ๐ ) โ ( V โ 1o ) ) ) |
187 |
186
|
anbi2d |
โข ( ๐ โ ( ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ โ
) โ ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ ( V โ 1o ) ) ) ) |
188 |
184 187
|
bitrd |
โข ( ๐ โ ( ๐ โ ( ๐บ supp โ
) โ ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ ( V โ 1o ) ) ) ) |
189 |
7
|
sseld |
โข ( ๐ โ ( ๐ โ ( ๐บ supp โ
) โ ๐ โ ๐ ) ) |
190 |
188 189
|
sylbird |
โข ( ๐ โ ( ( ๐ โ ๐ต โง ( ๐บ โ ๐ ) โ ( V โ 1o ) ) โ ๐ โ ๐ ) ) |
191 |
5 190
|
mpand |
โข ( ๐ โ ( ( ๐บ โ ๐ ) โ ( V โ 1o ) โ ๐ โ ๐ ) ) |
192 |
181 191
|
syl5bir |
โข ( ๐ โ ( ( ๐บ โ ๐ ) โ โ
โ ๐ โ ๐ ) ) |
193 |
192
|
necon1bd |
โข ( ๐ โ ( ยฌ ๐ โ ๐ โ ( ๐บ โ ๐ ) = โ
) ) |
194 |
99 193
|
mpd |
โข ( ๐ โ ( ๐บ โ ๐ ) = โ
) |
195 |
194
|
adantr |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ๐บ โ ๐ ) = โ
) |
196 |
|
fveqeq2 |
โข ( ๐ = ๐ โ ( ( ๐บ โ ๐ ) = โ
โ ( ๐บ โ ๐ ) = โ
) ) |
197 |
195 196
|
syl5ibrcom |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ๐ = ๐ โ ( ๐บ โ ๐ ) = โ
) ) |
198 |
|
eldifi |
โข ( ๐ โ ( ๐ต โ ( ๐น supp โ
) ) โ ๐ โ ๐ต ) |
199 |
198
|
adantl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ๐ โ ๐ต ) |
200 |
6
|
adantr |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ๐ โ ๐ด ) |
201 |
200 110 111
|
sylancl |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) โ V ) |
202 |
8 106 199 201
|
fvmptd3 |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ๐น โ ๐ ) = if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) ) |
203 |
|
ssidd |
โข ( ๐ โ ( ๐น supp โ
) โ ( ๐น supp โ
) ) |
204 |
44 203 3 9
|
suppssr |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ๐น โ ๐ ) = โ
) |
205 |
202 204
|
eqtr3d |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) = โ
) |
206 |
|
iffalse |
โข ( ยฌ ๐ = ๐ โ if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) = ( ๐บ โ ๐ ) ) |
207 |
206
|
eqeq1d |
โข ( ยฌ ๐ = ๐ โ ( if ( ๐ = ๐ , ๐ , ( ๐บ โ ๐ ) ) = โ
โ ( ๐บ โ ๐ ) = โ
) ) |
208 |
205 207
|
syl5ibcom |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ยฌ ๐ = ๐ โ ( ๐บ โ ๐ ) = โ
) ) |
209 |
197 208
|
pm2.61d |
โข ( ( ๐ โง ๐ โ ( ๐ต โ ( ๐น supp โ
) ) ) โ ( ๐บ โ ๐ ) = โ
) |
210 |
41 209
|
suppss |
โข ( ๐ โ ( ๐บ supp โ
) โ ( ๐น supp โ
) ) |
211 |
|
reldisj |
โข ( ( ๐บ supp โ
) โ ( ๐น supp โ
) โ ( ( ( ๐บ supp โ
) โฉ { ๐ } ) = โ
โ ( ๐บ supp โ
) โ ( ( ๐น supp โ
) โ { ๐ } ) ) ) |
212 |
210 211
|
syl |
โข ( ๐ โ ( ( ( ๐บ supp โ
) โฉ { ๐ } ) = โ
โ ( ๐บ supp โ
) โ ( ( ๐น supp โ
) โ { ๐ } ) ) ) |
213 |
178 212
|
mpbid |
โข ( ๐ โ ( ๐บ supp โ
) โ ( ( ๐น supp โ
) โ { ๐ } ) ) |
214 |
|
uncom |
โข ( ( ๐บ supp โ
) โช { ๐ } ) = ( { ๐ } โช ( ๐บ supp โ
) ) |
215 |
129 214
|
sseqtrdi |
โข ( ๐ โ ( ๐น supp โ
) โ ( { ๐ } โช ( ๐บ supp โ
) ) ) |
216 |
|
ssundif |
โข ( ( ๐น supp โ
) โ ( { ๐ } โช ( ๐บ supp โ
) ) โ ( ( ๐น supp โ
) โ { ๐ } ) โ ( ๐บ supp โ
) ) |
217 |
215 216
|
sylib |
โข ( ๐ โ ( ( ๐น supp โ
) โ { ๐ } ) โ ( ๐บ supp โ
) ) |
218 |
213 217
|
eqssd |
โข ( ๐ โ ( ๐บ supp โ
) = ( ( ๐น supp โ
) โ { ๐ } ) ) |
219 |
157 175 218
|
3eqtr4rd |
โข ( ๐ โ ( ๐บ supp โ
) = ( ๐ โ โช dom ๐ ) ) |
220 |
|
isores3 |
โข ( ( ๐ Isom E , E ( dom ๐ , ( ๐น supp โ
) ) โง โช dom ๐ โ dom ๐ โง ( ๐บ supp โ
) = ( ๐ โ โช dom ๐ ) ) โ ( ๐ โพ โช dom ๐ ) Isom E , E ( โช dom ๐ , ( ๐บ supp โ
) ) ) |
221 |
28 146 219 220
|
syl3anc |
โข ( ๐ โ ( ๐ โพ โช dom ๐ ) Isom E , E ( โช dom ๐ , ( ๐บ supp โ
) ) ) |
222 |
1 2 3 12 4
|
cantnfcl |
โข ( ๐ โ ( E We ( ๐บ supp โ
) โง dom ๐พ โ ฯ ) ) |
223 |
222
|
simpld |
โข ( ๐ โ E We ( ๐บ supp โ
) ) |
224 |
|
epse |
โข E Se ( ๐บ supp โ
) |
225 |
12
|
oieu |
โข ( ( E We ( ๐บ supp โ
) โง E Se ( ๐บ supp โ
) ) โ ( ( Ord โช dom ๐ โง ( ๐ โพ โช dom ๐ ) Isom E , E ( โช dom ๐ , ( ๐บ supp โ
) ) ) โ ( โช dom ๐ = dom ๐พ โง ( ๐ โพ โช dom ๐ ) = ๐พ ) ) ) |
226 |
223 224 225
|
sylancl |
โข ( ๐ โ ( ( Ord โช dom ๐ โง ( ๐ โพ โช dom ๐ ) Isom E , E ( โช dom ๐ , ( ๐บ supp โ
) ) ) โ ( โช dom ๐ = dom ๐พ โง ( ๐ โพ โช dom ๐ ) = ๐พ ) ) ) |
227 |
144 221 226
|
mpbi2and |
โข ( ๐ โ ( โช dom ๐ = dom ๐พ โง ( ๐ โพ โช dom ๐ ) = ๐พ ) ) |
228 |
227
|
simpld |
โข ( ๐ โ โช dom ๐ = dom ๐พ ) |
229 |
228
|
fveq2d |
โข ( ๐ โ ( ๐ โ โช dom ๐ ) = ( ๐ โ dom ๐พ ) ) |
230 |
|
eleq1 |
โข ( ๐ฅ = โ
โ ( ๐ฅ โ dom ๐ โ โ
โ dom ๐ ) ) |
231 |
|
fveq2 |
โข ( ๐ฅ = โ
โ ( ๐ป โ ๐ฅ ) = ( ๐ป โ โ
) ) |
232 |
|
fveq2 |
โข ( ๐ฅ = โ
โ ( ๐ โ ๐ฅ ) = ( ๐ โ โ
) ) |
233 |
13
|
seqom0g |
โข ( โ
โ V โ ( ๐ โ โ
) = โ
) |
234 |
46 233
|
ax-mp |
โข ( ๐ โ โ
) = โ
|
235 |
232 234
|
eqtrdi |
โข ( ๐ฅ = โ
โ ( ๐ โ ๐ฅ ) = โ
) |
236 |
231 235
|
eqeq12d |
โข ( ๐ฅ = โ
โ ( ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) โ ( ๐ป โ โ
) = โ
) ) |
237 |
230 236
|
imbi12d |
โข ( ๐ฅ = โ
โ ( ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) โ ( โ
โ dom ๐ โ ( ๐ป โ โ
) = โ
) ) ) |
238 |
237
|
imbi2d |
โข ( ๐ฅ = โ
โ ( ( ๐ โ ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) ) โ ( ๐ โ ( โ
โ dom ๐ โ ( ๐ป โ โ
) = โ
) ) ) ) |
239 |
|
eleq1 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ฅ โ dom ๐ โ ๐ฆ โ dom ๐ ) ) |
240 |
|
fveq2 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ป โ ๐ฅ ) = ( ๐ป โ ๐ฆ ) ) |
241 |
|
fveq2 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ โ ๐ฅ ) = ( ๐ โ ๐ฆ ) ) |
242 |
240 241
|
eqeq12d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) |
243 |
239 242
|
imbi12d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) โ ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) ) |
244 |
243
|
imbi2d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ โ ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) ) โ ( ๐ โ ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) ) ) |
245 |
|
eleq1 |
โข ( ๐ฅ = suc ๐ฆ โ ( ๐ฅ โ dom ๐ โ suc ๐ฆ โ dom ๐ ) ) |
246 |
|
fveq2 |
โข ( ๐ฅ = suc ๐ฆ โ ( ๐ป โ ๐ฅ ) = ( ๐ป โ suc ๐ฆ ) ) |
247 |
|
fveq2 |
โข ( ๐ฅ = suc ๐ฆ โ ( ๐ โ ๐ฅ ) = ( ๐ โ suc ๐ฆ ) ) |
248 |
246 247
|
eqeq12d |
โข ( ๐ฅ = suc ๐ฆ โ ( ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) |
249 |
245 248
|
imbi12d |
โข ( ๐ฅ = suc ๐ฆ โ ( ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) |
250 |
249
|
imbi2d |
โข ( ๐ฅ = suc ๐ฆ โ ( ( ๐ โ ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) ) โ ( ๐ โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) ) |
251 |
|
eleq1 |
โข ( ๐ฅ = โช dom ๐ โ ( ๐ฅ โ dom ๐ โ โช dom ๐ โ dom ๐ ) ) |
252 |
|
fveq2 |
โข ( ๐ฅ = โช dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ป โ โช dom ๐ ) ) |
253 |
|
fveq2 |
โข ( ๐ฅ = โช dom ๐ โ ( ๐ โ ๐ฅ ) = ( ๐ โ โช dom ๐ ) ) |
254 |
252 253
|
eqeq12d |
โข ( ๐ฅ = โช dom ๐ โ ( ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) ) |
255 |
251 254
|
imbi12d |
โข ( ๐ฅ = โช dom ๐ โ ( ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) โ ( โช dom ๐ โ dom ๐ โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) ) ) |
256 |
255
|
imbi2d |
โข ( ๐ฅ = โช dom ๐ โ ( ( ๐ โ ( ๐ฅ โ dom ๐ โ ( ๐ป โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) ) โ ( ๐ โ ( โช dom ๐ โ dom ๐ โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) ) ) ) |
257 |
11
|
seqom0g |
โข ( โ
โ dom ๐ โ ( ๐ป โ โ
) = โ
) |
258 |
257
|
a1i |
โข ( ๐ โ ( โ
โ dom ๐ โ ( ๐ป โ โ
) = โ
) ) |
259 |
|
nnord |
โข ( dom ๐ โ ฯ โ Ord dom ๐ ) |
260 |
19 259
|
syl |
โข ( ๐ โ Ord dom ๐ ) |
261 |
|
ordtr |
โข ( Ord dom ๐ โ Tr dom ๐ ) |
262 |
260 261
|
syl |
โข ( ๐ โ Tr dom ๐ ) |
263 |
|
trsuc |
โข ( ( Tr dom ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ฆ โ dom ๐ ) |
264 |
262 263
|
sylan |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ฆ โ dom ๐ ) |
265 |
264
|
ex |
โข ( ๐ โ ( suc ๐ฆ โ dom ๐ โ ๐ฆ โ dom ๐ ) ) |
266 |
265
|
imim1d |
โข ( ๐ โ ( ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) ) |
267 |
|
oveq2 |
โข ( ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) โ ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ป โ ๐ฆ ) ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) |
268 |
|
elnn |
โข ( ( ๐ฆ โ dom ๐ โง dom ๐ โ ฯ ) โ ๐ฆ โ ฯ ) |
269 |
268
|
ancoms |
โข ( ( dom ๐ โ ฯ โง ๐ฆ โ dom ๐ ) โ ๐ฆ โ ฯ ) |
270 |
19 264 269
|
syl2an2r |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ฆ โ ฯ ) |
271 |
1 2 3 10 14 11
|
cantnfsuc |
โข ( ( ๐ โง ๐ฆ โ ฯ ) โ ( ๐ป โ suc ๐ฆ ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ป โ ๐ฆ ) ) ) |
272 |
270 271
|
syldan |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐ป โ suc ๐ฆ ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ป โ ๐ฆ ) ) ) |
273 |
1 2 3 12 4 13
|
cantnfsuc |
โข ( ( ๐ โง ๐ฆ โ ฯ ) โ ( ๐ โ suc ๐ฆ ) = ( ( ( ๐ด โo ( ๐พ โ ๐ฆ ) ) ยทo ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) |
274 |
270 273
|
syldan |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐ โ suc ๐ฆ ) = ( ( ( ๐ด โo ( ๐พ โ ๐ฆ ) ) ยทo ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) |
275 |
227
|
simprd |
โข ( ๐ โ ( ๐ โพ โช dom ๐ ) = ๐พ ) |
276 |
275
|
fveq1d |
โข ( ๐ โ ( ( ๐ โพ โช dom ๐ ) โ ๐ฆ ) = ( ๐พ โ ๐ฆ ) ) |
277 |
276
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ๐ โพ โช dom ๐ ) โ ๐ฆ ) = ( ๐พ โ ๐ฆ ) ) |
278 |
16
|
eleq2d |
โข ( ๐ โ ( suc ๐ฆ โ dom ๐ โ suc ๐ฆ โ suc โช dom ๐ ) ) |
279 |
278
|
biimpa |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ suc ๐ฆ โ suc โช dom ๐ ) |
280 |
144
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ Ord โช dom ๐ ) |
281 |
|
ordsucelsuc |
โข ( Ord โช dom ๐ โ ( ๐ฆ โ โช dom ๐ โ suc ๐ฆ โ suc โช dom ๐ ) ) |
282 |
280 281
|
syl |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐ฆ โ โช dom ๐ โ suc ๐ฆ โ suc โช dom ๐ ) ) |
283 |
279 282
|
mpbird |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ฆ โ โช dom ๐ ) |
284 |
283
|
fvresd |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ๐ โพ โช dom ๐ ) โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) |
285 |
277 284
|
eqtr3d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐พ โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) |
286 |
285
|
oveq2d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐ด โo ( ๐พ โ ๐ฆ ) ) = ( ๐ด โo ( ๐ โ ๐ฆ ) ) ) |
287 |
|
eqeq1 |
โข ( ๐ก = ( ๐พ โ ๐ฆ ) โ ( ๐ก = ๐ โ ( ๐พ โ ๐ฆ ) = ๐ ) ) |
288 |
|
fveq2 |
โข ( ๐ก = ( ๐พ โ ๐ฆ ) โ ( ๐บ โ ๐ก ) = ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) |
289 |
287 288
|
ifbieq2d |
โข ( ๐ก = ( ๐พ โ ๐ฆ ) โ if ( ๐ก = ๐ , ๐ , ( ๐บ โ ๐ก ) ) = if ( ( ๐พ โ ๐ฆ ) = ๐ , ๐ , ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) ) |
290 |
|
suppssdm |
โข ( ๐บ supp โ
) โ dom ๐บ |
291 |
290 41
|
fssdm |
โข ( ๐ โ ( ๐บ supp โ
) โ ๐ต ) |
292 |
291
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐บ supp โ
) โ ๐ต ) |
293 |
228
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ โช dom ๐ = dom ๐พ ) |
294 |
283 293
|
eleqtrd |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ฆ โ dom ๐พ ) |
295 |
12
|
oif |
โข ๐พ : dom ๐พ โถ ( ๐บ supp โ
) |
296 |
295
|
ffvelrni |
โข ( ๐ฆ โ dom ๐พ โ ( ๐พ โ ๐ฆ ) โ ( ๐บ supp โ
) ) |
297 |
294 296
|
syl |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐พ โ ๐ฆ ) โ ( ๐บ supp โ
) ) |
298 |
292 297
|
sseldd |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐พ โ ๐ฆ ) โ ๐ต ) |
299 |
6
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ๐ โ ๐ด ) |
300 |
|
fvex |
โข ( ๐บ โ ( ๐พ โ ๐ฆ ) ) โ V |
301 |
|
ifexg |
โข ( ( ๐ โ ๐ด โง ( ๐บ โ ( ๐พ โ ๐ฆ ) ) โ V ) โ if ( ( ๐พ โ ๐ฆ ) = ๐ , ๐ , ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) โ V ) |
302 |
299 300 301
|
sylancl |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ if ( ( ๐พ โ ๐ฆ ) = ๐ , ๐ , ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) โ V ) |
303 |
8 289 298 302
|
fvmptd3 |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐น โ ( ๐พ โ ๐ฆ ) ) = if ( ( ๐พ โ ๐ฆ ) = ๐ , ๐ , ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) ) |
304 |
285
|
fveq2d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐น โ ( ๐พ โ ๐ฆ ) ) = ( ๐น โ ( ๐ โ ๐ฆ ) ) ) |
305 |
176
|
adantr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ยฌ ๐ โ ( ๐บ supp โ
) ) |
306 |
|
nelneq |
โข ( ( ( ๐พ โ ๐ฆ ) โ ( ๐บ supp โ
) โง ยฌ ๐ โ ( ๐บ supp โ
) ) โ ยฌ ( ๐พ โ ๐ฆ ) = ๐ ) |
307 |
297 305 306
|
syl2anc |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ยฌ ( ๐พ โ ๐ฆ ) = ๐ ) |
308 |
307
|
iffalsed |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ if ( ( ๐พ โ ๐ฆ ) = ๐ , ๐ , ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) = ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) |
309 |
303 304 308
|
3eqtr3rd |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐บ โ ( ๐พ โ ๐ฆ ) ) = ( ๐น โ ( ๐ โ ๐ฆ ) ) ) |
310 |
286 309
|
oveq12d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ๐ด โo ( ๐พ โ ๐ฆ ) ) ยทo ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) = ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) ) |
311 |
310
|
oveq1d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ( ๐ด โo ( ๐พ โ ๐ฆ ) ) ยทo ( ๐บ โ ( ๐พ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) |
312 |
274 311
|
eqtrd |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ๐ โ suc ๐ฆ ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) |
313 |
272 312
|
eqeq12d |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) โ ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ป โ ๐ฆ ) ) = ( ( ( ๐ด โo ( ๐ โ ๐ฆ ) ) ยทo ( ๐น โ ( ๐ โ ๐ฆ ) ) ) +o ( ๐ โ ๐ฆ ) ) ) ) |
314 |
267 313
|
syl5ibr |
โข ( ( ๐ โง suc ๐ฆ โ dom ๐ ) โ ( ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) |
315 |
314
|
ex |
โข ( ๐ โ ( suc ๐ฆ โ dom ๐ โ ( ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) |
316 |
315
|
a2d |
โข ( ๐ โ ( ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) |
317 |
266 316
|
syld |
โข ( ๐ โ ( ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) |
318 |
317
|
a2i |
โข ( ( ๐ โ ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) โ ( ๐ โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) |
319 |
318
|
a1i |
โข ( ๐ฆ โ ฯ โ ( ( ๐ โ ( ๐ฆ โ dom ๐ โ ( ๐ป โ ๐ฆ ) = ( ๐ โ ๐ฆ ) ) ) โ ( ๐ โ ( suc ๐ฆ โ dom ๐ โ ( ๐ป โ suc ๐ฆ ) = ( ๐ โ suc ๐ฆ ) ) ) ) ) |
320 |
238 244 250 256 258 319
|
finds |
โข ( โช dom ๐ โ ฯ โ ( ๐ โ ( โช dom ๐ โ dom ๐ โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) ) ) |
321 |
22 320
|
mpcom |
โข ( ๐ โ ( โช dom ๐ โ dom ๐ โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) ) |
322 |
64 321
|
mpd |
โข ( ๐ โ ( ๐ป โ โช dom ๐ ) = ( ๐ โ โช dom ๐ ) ) |
323 |
1 2 3 12 4 13
|
cantnfval |
โข ( ๐ โ ( ( ๐ด CNF ๐ต ) โ ๐บ ) = ( ๐ โ dom ๐พ ) ) |
324 |
229 322 323
|
3eqtr4d |
โข ( ๐ โ ( ๐ป โ โช dom ๐ ) = ( ( ๐ด CNF ๐ต ) โ ๐บ ) ) |
325 |
142 324
|
oveq12d |
โข ( ๐ โ ( ( ( ๐ด โo ( ๐ โ โช dom ๐ ) ) ยทo ( ๐น โ ( ๐ โ โช dom ๐ ) ) ) +o ( ๐ป โ โช dom ๐ ) ) = ( ( ( ๐ด โo ๐ ) ยทo ๐ ) +o ( ( ๐ด CNF ๐ต ) โ ๐บ ) ) ) |
326 |
24 325
|
eqtrd |
โข ( ๐ โ ( ๐ป โ suc โช dom ๐ ) = ( ( ( ๐ด โo ๐ ) ยทo ๐ ) +o ( ( ๐ด CNF ๐ต ) โ ๐บ ) ) ) |
327 |
15 17 326
|
3eqtrd |
โข ( ๐ โ ( ( ๐ด CNF ๐ต ) โ ๐น ) = ( ( ( ๐ด โo ๐ ) ยทo ๐ ) +o ( ( ๐ด CNF ๐ต ) โ ๐บ ) ) ) |