Step |
Hyp |
Ref |
Expression |
1 |
|
cnfcom.s |
โข ๐ = dom ( ฯ CNF ๐ด ) |
2 |
|
cnfcom.a |
โข ( ๐ โ ๐ด โ On ) |
3 |
|
cnfcom.b |
โข ( ๐ โ ๐ต โ ( ฯ โo ๐ด ) ) |
4 |
|
cnfcom.f |
โข ๐น = ( โก ( ฯ CNF ๐ด ) โ ๐ต ) |
5 |
|
cnfcom.g |
โข ๐บ = OrdIso ( E , ( ๐น supp โ
) ) |
6 |
|
cnfcom.h |
โข ๐ป = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ๐ +o ๐ง ) ) , โ
) |
7 |
|
cnfcom.t |
โข ๐ = seqฯ ( ( ๐ โ V , ๐ โ V โฆ ๐พ ) , โ
) |
8 |
|
cnfcom.m |
โข ๐ = ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) |
9 |
|
cnfcom.k |
โข ๐พ = ( ( ๐ฅ โ ๐ โฆ ( dom ๐ +o ๐ฅ ) ) โช โก ( ๐ฅ โ dom ๐ โฆ ( ๐ +o ๐ฅ ) ) ) |
10 |
|
cnfcom.1 |
โข ( ๐ โ ๐ผ โ dom ๐บ ) |
11 |
|
cnfcom.2 |
โข ( ๐ โ ๐ โ ( ฯ โo ( ๐บ โ ๐ผ ) ) ) |
12 |
|
cnfcom.3 |
โข ( ๐ โ ( ๐ โ ๐ผ ) : ( ๐ป โ ๐ผ ) โ1-1-ontoโ ๐ ) |
13 |
|
omelon |
โข ฯ โ On |
14 |
|
suppssdm |
โข ( ๐น supp โ
) โ dom ๐น |
15 |
13
|
a1i |
โข ( ๐ โ ฯ โ On ) |
16 |
1 15 2
|
cantnff1o |
โข ( ๐ โ ( ฯ CNF ๐ด ) : ๐ โ1-1-ontoโ ( ฯ โo ๐ด ) ) |
17 |
|
f1ocnv |
โข ( ( ฯ CNF ๐ด ) : ๐ โ1-1-ontoโ ( ฯ โo ๐ด ) โ โก ( ฯ CNF ๐ด ) : ( ฯ โo ๐ด ) โ1-1-ontoโ ๐ ) |
18 |
|
f1of |
โข ( โก ( ฯ CNF ๐ด ) : ( ฯ โo ๐ด ) โ1-1-ontoโ ๐ โ โก ( ฯ CNF ๐ด ) : ( ฯ โo ๐ด ) โถ ๐ ) |
19 |
16 17 18
|
3syl |
โข ( ๐ โ โก ( ฯ CNF ๐ด ) : ( ฯ โo ๐ด ) โถ ๐ ) |
20 |
19 3
|
ffvelrnd |
โข ( ๐ โ ( โก ( ฯ CNF ๐ด ) โ ๐ต ) โ ๐ ) |
21 |
4 20
|
eqeltrid |
โข ( ๐ โ ๐น โ ๐ ) |
22 |
1 15 2
|
cantnfs |
โข ( ๐ โ ( ๐น โ ๐ โ ( ๐น : ๐ด โถ ฯ โง ๐น finSupp โ
) ) ) |
23 |
21 22
|
mpbid |
โข ( ๐ โ ( ๐น : ๐ด โถ ฯ โง ๐น finSupp โ
) ) |
24 |
23
|
simpld |
โข ( ๐ โ ๐น : ๐ด โถ ฯ ) |
25 |
14 24
|
fssdm |
โข ( ๐ โ ( ๐น supp โ
) โ ๐ด ) |
26 |
5
|
oif |
โข ๐บ : dom ๐บ โถ ( ๐น supp โ
) |
27 |
26
|
ffvelrni |
โข ( ๐ผ โ dom ๐บ โ ( ๐บ โ ๐ผ ) โ ( ๐น supp โ
) ) |
28 |
10 27
|
syl |
โข ( ๐ โ ( ๐บ โ ๐ผ ) โ ( ๐น supp โ
) ) |
29 |
25 28
|
sseldd |
โข ( ๐ โ ( ๐บ โ ๐ผ ) โ ๐ด ) |
30 |
|
onelon |
โข ( ( ๐ด โ On โง ( ๐บ โ ๐ผ ) โ ๐ด ) โ ( ๐บ โ ๐ผ ) โ On ) |
31 |
2 29 30
|
syl2anc |
โข ( ๐ โ ( ๐บ โ ๐ผ ) โ On ) |
32 |
|
oecl |
โข ( ( ฯ โ On โง ( ๐บ โ ๐ผ ) โ On ) โ ( ฯ โo ( ๐บ โ ๐ผ ) ) โ On ) |
33 |
13 31 32
|
sylancr |
โข ( ๐ โ ( ฯ โo ( ๐บ โ ๐ผ ) ) โ On ) |
34 |
24 29
|
ffvelrnd |
โข ( ๐ โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ ฯ ) |
35 |
|
nnon |
โข ( ( ๐น โ ( ๐บ โ ๐ผ ) ) โ ฯ โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ On ) |
36 |
34 35
|
syl |
โข ( ๐ โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ On ) |
37 |
|
omcl |
โข ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) โ On โง ( ๐น โ ( ๐บ โ ๐ผ ) ) โ On ) โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ On ) |
38 |
33 36 37
|
syl2anc |
โข ( ๐ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ On ) |
39 |
1 15 2 5 21
|
cantnfcl |
โข ( ๐ โ ( E We ( ๐น supp โ
) โง dom ๐บ โ ฯ ) ) |
40 |
39
|
simprd |
โข ( ๐ โ dom ๐บ โ ฯ ) |
41 |
|
elnn |
โข ( ( ๐ผ โ dom ๐บ โง dom ๐บ โ ฯ ) โ ๐ผ โ ฯ ) |
42 |
10 40 41
|
syl2anc |
โข ( ๐ โ ๐ผ โ ฯ ) |
43 |
6
|
cantnfvalf |
โข ๐ป : ฯ โถ On |
44 |
43
|
ffvelrni |
โข ( ๐ผ โ ฯ โ ( ๐ป โ ๐ผ ) โ On ) |
45 |
42 44
|
syl |
โข ( ๐ โ ( ๐ป โ ๐ผ ) โ On ) |
46 |
|
eqid |
โข ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) |
47 |
46
|
oacomf1o |
โข ( ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ On โง ( ๐ป โ ๐ผ ) โ On ) โ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) |
48 |
38 45 47
|
syl2anc |
โข ( ๐ โ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) |
49 |
7
|
seqomsuc |
โข ( ๐ผ โ ฯ โ ( ๐ โ suc ๐ผ ) = ( ๐ผ ( ๐ โ V , ๐ โ V โฆ ๐พ ) ( ๐ โ ๐ผ ) ) ) |
50 |
42 49
|
syl |
โข ( ๐ โ ( ๐ โ suc ๐ผ ) = ( ๐ผ ( ๐ โ V , ๐ โ V โฆ ๐พ ) ( ๐ โ ๐ผ ) ) ) |
51 |
|
nfcv |
โข โฒ ๐ข ๐พ |
52 |
|
nfcv |
โข โฒ ๐ฃ ๐พ |
53 |
|
nfcv |
โข โฒ ๐ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) |
54 |
|
nfcv |
โข โฒ ๐ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) |
55 |
|
oveq2 |
โข ( ๐ฅ = ๐ฆ โ ( dom ๐ +o ๐ฅ ) = ( dom ๐ +o ๐ฆ ) ) |
56 |
55
|
cbvmptv |
โข ( ๐ฅ โ ๐ โฆ ( dom ๐ +o ๐ฅ ) ) = ( ๐ฆ โ ๐ โฆ ( dom ๐ +o ๐ฆ ) ) |
57 |
|
simpl |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ๐ = ๐ข ) |
58 |
57
|
fveq2d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐บ โ ๐ ) = ( ๐บ โ ๐ข ) ) |
59 |
58
|
oveq2d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ฯ โo ( ๐บ โ ๐ ) ) = ( ฯ โo ( ๐บ โ ๐ข ) ) ) |
60 |
58
|
fveq2d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐น โ ( ๐บ โ ๐ ) ) = ( ๐น โ ( ๐บ โ ๐ข ) ) ) |
61 |
59 60
|
oveq12d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) = ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) ) |
62 |
8 61
|
eqtrid |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ๐ = ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) ) |
63 |
|
simpr |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ๐ = ๐ฃ ) |
64 |
63
|
dmeqd |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ dom ๐ = dom ๐ฃ ) |
65 |
64
|
oveq1d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( dom ๐ +o ๐ฆ ) = ( dom ๐ฃ +o ๐ฆ ) ) |
66 |
62 65
|
mpteq12dv |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐ฆ โ ๐ โฆ ( dom ๐ +o ๐ฆ ) ) = ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) ) |
67 |
56 66
|
eqtrid |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐ฅ โ ๐ โฆ ( dom ๐ +o ๐ฅ ) ) = ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) ) |
68 |
|
oveq2 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ +o ๐ฅ ) = ( ๐ +o ๐ฆ ) ) |
69 |
68
|
cbvmptv |
โข ( ๐ฅ โ dom ๐ โฆ ( ๐ +o ๐ฅ ) ) = ( ๐ฆ โ dom ๐ โฆ ( ๐ +o ๐ฆ ) ) |
70 |
62
|
oveq1d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐ +o ๐ฆ ) = ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) |
71 |
64 70
|
mpteq12dv |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐ฆ โ dom ๐ โฆ ( ๐ +o ๐ฆ ) ) = ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) |
72 |
69 71
|
eqtrid |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ๐ฅ โ dom ๐ โฆ ( ๐ +o ๐ฅ ) ) = ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) |
73 |
72
|
cnveqd |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ โก ( ๐ฅ โ dom ๐ โฆ ( ๐ +o ๐ฅ ) ) = โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) |
74 |
67 73
|
uneq12d |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ( ( ๐ฅ โ ๐ โฆ ( dom ๐ +o ๐ฅ ) ) โช โก ( ๐ฅ โ dom ๐ โฆ ( ๐ +o ๐ฅ ) ) ) = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) ) |
75 |
9 74
|
eqtrid |
โข ( ( ๐ = ๐ข โง ๐ = ๐ฃ ) โ ๐พ = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) ) |
76 |
51 52 53 54 75
|
cbvmpo |
โข ( ๐ โ V , ๐ โ V โฆ ๐พ ) = ( ๐ข โ V , ๐ฃ โ V โฆ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) ) |
77 |
76
|
a1i |
โข ( ๐ โ ( ๐ โ V , ๐ โ V โฆ ๐พ ) = ( ๐ข โ V , ๐ฃ โ V โฆ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) ) ) |
78 |
|
simprl |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ๐ข = ๐ผ ) |
79 |
78
|
fveq2d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ๐บ โ ๐ข ) = ( ๐บ โ ๐ผ ) ) |
80 |
79
|
oveq2d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ฯ โo ( ๐บ โ ๐ข ) ) = ( ฯ โo ( ๐บ โ ๐ผ ) ) ) |
81 |
79
|
fveq2d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ๐น โ ( ๐บ โ ๐ข ) ) = ( ๐น โ ( ๐บ โ ๐ผ ) ) ) |
82 |
80 81
|
oveq12d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) = ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |
83 |
|
simpr |
โข ( ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) โ ๐ฃ = ( ๐ โ ๐ผ ) ) |
84 |
83
|
dmeqd |
โข ( ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) โ dom ๐ฃ = dom ( ๐ โ ๐ผ ) ) |
85 |
|
f1odm |
โข ( ( ๐ โ ๐ผ ) : ( ๐ป โ ๐ผ ) โ1-1-ontoโ ๐ โ dom ( ๐ โ ๐ผ ) = ( ๐ป โ ๐ผ ) ) |
86 |
12 85
|
syl |
โข ( ๐ โ dom ( ๐ โ ๐ผ ) = ( ๐ป โ ๐ผ ) ) |
87 |
84 86
|
sylan9eqr |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ dom ๐ฃ = ( ๐ป โ ๐ผ ) ) |
88 |
87
|
oveq1d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( dom ๐ฃ +o ๐ฆ ) = ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) |
89 |
82 88
|
mpteq12dv |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) = ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) ) |
90 |
82
|
oveq1d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) = ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) |
91 |
87 90
|
mpteq12dv |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) = ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) |
92 |
91
|
cnveqd |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) = โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) |
93 |
89 92
|
uneq12d |
โข ( ( ๐ โง ( ๐ข = ๐ผ โง ๐ฃ = ( ๐ โ ๐ผ ) ) ) โ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) โฆ ( dom ๐ฃ +o ๐ฆ ) ) โช โก ( ๐ฆ โ dom ๐ฃ โฆ ( ( ( ฯ โo ( ๐บ โ ๐ข ) ) ยทo ( ๐น โ ( ๐บ โ ๐ข ) ) ) +o ๐ฆ ) ) ) = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) ) |
94 |
10
|
elexd |
โข ( ๐ โ ๐ผ โ V ) |
95 |
|
fvexd |
โข ( ๐ โ ( ๐ โ ๐ผ ) โ V ) |
96 |
|
ovex |
โข ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ V |
97 |
96
|
mptex |
โข ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โ V |
98 |
|
fvex |
โข ( ๐ป โ ๐ผ ) โ V |
99 |
98
|
mptex |
โข ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) โ V |
100 |
99
|
cnvex |
โข โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) โ V |
101 |
97 100
|
unex |
โข ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) โ V |
102 |
101
|
a1i |
โข ( ๐ โ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) โ V ) |
103 |
77 93 94 95 102
|
ovmpod |
โข ( ๐ โ ( ๐ผ ( ๐ โ V , ๐ โ V โฆ ๐พ ) ( ๐ โ ๐ผ ) ) = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) ) |
104 |
50 103
|
eqtrd |
โข ( ๐ โ ( ๐ โ suc ๐ผ ) = ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) ) |
105 |
104
|
f1oeq1d |
โข ( ๐ โ ( ( ๐ โ suc ๐ผ ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) โ ( ( ๐ฆ โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โฆ ( ( ๐ป โ ๐ผ ) +o ๐ฆ ) ) โช โก ( ๐ฆ โ ( ๐ป โ ๐ผ ) โฆ ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ๐ฆ ) ) ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) ) |
106 |
48 105
|
mpbird |
โข ( ๐ โ ( ๐ โ suc ๐ผ ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) |
107 |
13
|
a1i |
โข ( ( ๐ด โ On โง ๐น โ ๐ ) โ ฯ โ On ) |
108 |
|
simpl |
โข ( ( ๐ด โ On โง ๐น โ ๐ ) โ ๐ด โ On ) |
109 |
|
simpr |
โข ( ( ๐ด โ On โง ๐น โ ๐ ) โ ๐น โ ๐ ) |
110 |
8
|
oveq1i |
โข ( ๐ +o ๐ง ) = ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) |
111 |
110
|
a1i |
โข ( ( ๐ โ V โง ๐ง โ V ) โ ( ๐ +o ๐ง ) = ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) |
112 |
111
|
mpoeq3ia |
โข ( ๐ โ V , ๐ง โ V โฆ ( ๐ +o ๐ง ) ) = ( ๐ โ V , ๐ง โ V โฆ ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) |
113 |
|
eqid |
โข โ
= โ
|
114 |
|
seqomeq12 |
โข ( ( ( ๐ โ V , ๐ง โ V โฆ ( ๐ +o ๐ง ) ) = ( ๐ โ V , ๐ง โ V โฆ ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) โง โ
= โ
) โ seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ๐ +o ๐ง ) ) , โ
) = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) , โ
) ) |
115 |
112 113 114
|
mp2an |
โข seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ๐ +o ๐ง ) ) , โ
) = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) , โ
) |
116 |
6 115
|
eqtri |
โข ๐ป = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ฯ โo ( ๐บ โ ๐ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ ) ) ) +o ๐ง ) ) , โ
) |
117 |
1 107 108 5 109 116
|
cantnfsuc |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ๐ผ โ ฯ ) โ ( ๐ป โ suc ๐ผ ) = ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) ) |
118 |
2 21 42 117
|
syl21anc |
โข ( ๐ โ ( ๐ป โ suc ๐ผ ) = ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) ) |
119 |
118
|
f1oeq2d |
โข ( ๐ โ ( ( ๐ โ suc ๐ผ ) : ( ๐ป โ suc ๐ผ ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) โ ( ๐ โ suc ๐ผ ) : ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) +o ( ๐ป โ ๐ผ ) ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) ) |
120 |
106 119
|
mpbird |
โข ( ๐ โ ( ๐ โ suc ๐ผ ) : ( ๐ป โ suc ๐ผ ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) |
121 |
|
sssucid |
โข dom ๐บ โ suc dom ๐บ |
122 |
121 10
|
sselid |
โข ( ๐ โ ๐ผ โ suc dom ๐บ ) |
123 |
|
epelg |
โข ( ๐ผ โ dom ๐บ โ ( ๐ฆ E ๐ผ โ ๐ฆ โ ๐ผ ) ) |
124 |
10 123
|
syl |
โข ( ๐ โ ( ๐ฆ E ๐ผ โ ๐ฆ โ ๐ผ ) ) |
125 |
124
|
biimpar |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ๐ฆ E ๐ผ ) |
126 |
|
ovexd |
โข ( ๐ โ ( ๐น supp โ
) โ V ) |
127 |
39
|
simpld |
โข ( ๐ โ E We ( ๐น supp โ
) ) |
128 |
5
|
oiiso |
โข ( ( ( ๐น supp โ
) โ V โง E We ( ๐น supp โ
) ) โ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โ
) ) ) |
129 |
126 127 128
|
syl2anc |
โข ( ๐ โ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โ
) ) ) |
130 |
129
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โ
) ) ) |
131 |
5
|
oicl |
โข Ord dom ๐บ |
132 |
|
ordelss |
โข ( ( Ord dom ๐บ โง ๐ผ โ dom ๐บ ) โ ๐ผ โ dom ๐บ ) |
133 |
131 10 132
|
sylancr |
โข ( ๐ โ ๐ผ โ dom ๐บ ) |
134 |
133
|
sselda |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ๐ฆ โ dom ๐บ ) |
135 |
10
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ๐ผ โ dom ๐บ ) |
136 |
|
isorel |
โข ( ( ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โ
) ) โง ( ๐ฆ โ dom ๐บ โง ๐ผ โ dom ๐บ ) ) โ ( ๐ฆ E ๐ผ โ ( ๐บ โ ๐ฆ ) E ( ๐บ โ ๐ผ ) ) ) |
137 |
130 134 135 136
|
syl12anc |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ( ๐ฆ E ๐ผ โ ( ๐บ โ ๐ฆ ) E ( ๐บ โ ๐ผ ) ) ) |
138 |
125 137
|
mpbid |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ( ๐บ โ ๐ฆ ) E ( ๐บ โ ๐ผ ) ) |
139 |
|
fvex |
โข ( ๐บ โ ๐ผ ) โ V |
140 |
139
|
epeli |
โข ( ( ๐บ โ ๐ฆ ) E ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ฆ ) โ ( ๐บ โ ๐ผ ) ) |
141 |
138 140
|
sylib |
โข ( ( ๐ โง ๐ฆ โ ๐ผ ) โ ( ๐บ โ ๐ฆ ) โ ( ๐บ โ ๐ผ ) ) |
142 |
141
|
ralrimiva |
โข ( ๐ โ โ ๐ฆ โ ๐ผ ( ๐บ โ ๐ฆ ) โ ( ๐บ โ ๐ผ ) ) |
143 |
|
ffun |
โข ( ๐บ : dom ๐บ โถ ( ๐น supp โ
) โ Fun ๐บ ) |
144 |
26 143
|
ax-mp |
โข Fun ๐บ |
145 |
|
funimass4 |
โข ( ( Fun ๐บ โง ๐ผ โ dom ๐บ ) โ ( ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) โ โ ๐ฆ โ ๐ผ ( ๐บ โ ๐ฆ ) โ ( ๐บ โ ๐ผ ) ) ) |
146 |
144 133 145
|
sylancr |
โข ( ๐ โ ( ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) โ โ ๐ฆ โ ๐ผ ( ๐บ โ ๐ฆ ) โ ( ๐บ โ ๐ผ ) ) ) |
147 |
142 146
|
mpbird |
โข ( ๐ โ ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) |
148 |
13
|
a1i |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ฯ โ On ) |
149 |
|
simpll |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ๐ด โ On ) |
150 |
|
simplr |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ๐น โ ๐ ) |
151 |
|
peano1 |
โข โ
โ ฯ |
152 |
151
|
a1i |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ โ
โ ฯ ) |
153 |
|
simpr1 |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ๐ผ โ suc dom ๐บ ) |
154 |
|
simpr2 |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ( ๐บ โ ๐ผ ) โ On ) |
155 |
|
simpr3 |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) |
156 |
1 148 149 5 150 116 152 153 154 155
|
cantnflt |
โข ( ( ( ๐ด โ On โง ๐น โ ๐ ) โง ( ๐ผ โ suc dom ๐บ โง ( ๐บ โ ๐ผ ) โ On โง ( ๐บ โ ๐ผ ) โ ( ๐บ โ ๐ผ ) ) ) โ ( ๐ป โ ๐ผ ) โ ( ฯ โo ( ๐บ โ ๐ผ ) ) ) |
157 |
2 21 122 31 147 156
|
syl23anc |
โข ( ๐ โ ( ๐ป โ ๐ผ ) โ ( ฯ โo ( ๐บ โ ๐ผ ) ) ) |
158 |
24
|
ffnd |
โข ( ๐ โ ๐น Fn ๐ด ) |
159 |
|
0ex |
โข โ
โ V |
160 |
159
|
a1i |
โข ( ๐ โ โ
โ V ) |
161 |
|
elsuppfn |
โข ( ( ๐น Fn ๐ด โง ๐ด โ On โง โ
โ V ) โ ( ( ๐บ โ ๐ผ ) โ ( ๐น supp โ
) โ ( ( ๐บ โ ๐ผ ) โ ๐ด โง ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) ) ) |
162 |
158 2 160 161
|
syl3anc |
โข ( ๐ โ ( ( ๐บ โ ๐ผ ) โ ( ๐น supp โ
) โ ( ( ๐บ โ ๐ผ ) โ ๐ด โง ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) ) ) |
163 |
|
simpr |
โข ( ( ( ๐บ โ ๐ผ ) โ ๐ด โง ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) |
164 |
162 163
|
syl6bi |
โข ( ๐ โ ( ( ๐บ โ ๐ผ ) โ ( ๐น supp โ
) โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) ) |
165 |
28 164
|
mpd |
โข ( ๐ โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) |
166 |
|
on0eln0 |
โข ( ( ๐น โ ( ๐บ โ ๐ผ ) ) โ On โ ( โ
โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) ) |
167 |
36 166
|
syl |
โข ( ๐ โ ( โ
โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ ( ๐น โ ( ๐บ โ ๐ผ ) ) โ โ
) ) |
168 |
165 167
|
mpbird |
โข ( ๐ โ โ
โ ( ๐น โ ( ๐บ โ ๐ผ ) ) ) |
169 |
|
omword1 |
โข ( ( ( ( ฯ โo ( ๐บ โ ๐ผ ) ) โ On โง ( ๐น โ ( ๐บ โ ๐ผ ) ) โ On ) โง โ
โ ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ ( ฯ โo ( ๐บ โ ๐ผ ) ) โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |
170 |
33 36 168 169
|
syl21anc |
โข ( ๐ โ ( ฯ โo ( ๐บ โ ๐ผ ) ) โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |
171 |
|
oaabs2 |
โข ( ( ( ( ๐ป โ ๐ผ ) โ ( ฯ โo ( ๐บ โ ๐ผ ) ) โง ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) โ On ) โง ( ฯ โo ( ๐บ โ ๐ผ ) ) โ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) โ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) = ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |
172 |
157 38 170 171
|
syl21anc |
โข ( ๐ โ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) = ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |
173 |
172
|
f1oeq3d |
โข ( ๐ โ ( ( ๐ โ suc ๐ผ ) : ( ๐ป โ suc ๐ผ ) โ1-1-ontoโ ( ( ๐ป โ ๐ผ ) +o ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) โ ( ๐ โ suc ๐ผ ) : ( ๐ป โ suc ๐ผ ) โ1-1-ontoโ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) ) |
174 |
120 173
|
mpbid |
โข ( ๐ โ ( ๐ โ suc ๐ผ ) : ( ๐ป โ suc ๐ผ ) โ1-1-ontoโ ( ( ฯ โo ( ๐บ โ ๐ผ ) ) ยทo ( ๐น โ ( ๐บ โ ๐ผ ) ) ) ) |