Step |
Hyp |
Ref |
Expression |
1 |
|
natfval.1 |
โข ๐ = ( ๐ถ Nat ๐ท ) |
2 |
|
natfval.b |
โข ๐ต = ( Base โ ๐ถ ) |
3 |
|
natfval.h |
โข ๐ป = ( Hom โ ๐ถ ) |
4 |
|
natfval.j |
โข ๐ฝ = ( Hom โ ๐ท ) |
5 |
|
natfval.o |
โข ยท = ( comp โ ๐ท ) |
6 |
|
oveq12 |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ๐ก Func ๐ข ) = ( ๐ถ Func ๐ท ) ) |
7 |
|
simpl |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ๐ก = ๐ถ ) |
8 |
7
|
fveq2d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Base โ ๐ก ) = ( Base โ ๐ถ ) ) |
9 |
8 2
|
eqtr4di |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Base โ ๐ก ) = ๐ต ) |
10 |
9
|
ixpeq1d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) = X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) ) |
11 |
|
simpr |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ๐ข = ๐ท ) |
12 |
11
|
fveq2d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Hom โ ๐ข ) = ( Hom โ ๐ท ) ) |
13 |
12 4
|
eqtr4di |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Hom โ ๐ข ) = ๐ฝ ) |
14 |
13
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) = ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) ) |
15 |
14
|
ixpeq2dv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) = X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) ) |
16 |
10 15
|
eqtrd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) = X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) ) |
17 |
7
|
fveq2d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Hom โ ๐ก ) = ( Hom โ ๐ถ ) ) |
18 |
17 3
|
eqtr4di |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( Hom โ ๐ก ) = ๐ป ) |
19 |
18
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) = ( ๐ฅ ๐ป ๐ฆ ) ) |
20 |
11
|
fveq2d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( comp โ ๐ข ) = ( comp โ ๐ท ) ) |
21 |
20 5
|
eqtr4di |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( comp โ ๐ข ) = ยท ) |
22 |
21
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) = ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ) |
23 |
22
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) ) |
24 |
21
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) = ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ) |
25 |
24
|
oveqd |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) ) |
26 |
23 25
|
eqeq12d |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) โ ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) ) ) |
27 |
19 26
|
raleqbidv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) โ โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) ) ) |
28 |
9 27
|
raleqbidv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) โ โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) ) ) |
29 |
9 28
|
raleqbidv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) ) ) |
30 |
16 29
|
rabeqbidv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ { ๐ โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } = { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) |
31 |
30
|
csbeq2dv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } = โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) |
32 |
31
|
csbeq2dv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } = โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) |
33 |
6 6 32
|
mpoeq123dv |
โข ( ( ๐ก = ๐ถ โง ๐ข = ๐ท ) โ ( ๐ โ ( ๐ก Func ๐ข ) , ๐ โ ( ๐ก Func ๐ข ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) = ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) ) |
34 |
|
df-nat |
โข Nat = ( ๐ก โ Cat , ๐ข โ Cat โฆ ( ๐ โ ( ๐ก Func ๐ข ) , ๐ โ ( ๐ก Func ๐ข ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ( Base โ ๐ก ) ( ( ๐ โ ๐ฅ ) ( Hom โ ๐ข ) ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ( Base โ ๐ก ) โ ๐ฆ โ ( Base โ ๐ก ) โ โ โ ( ๐ฅ ( Hom โ ๐ก ) ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ( comp โ ๐ข ) ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) ) |
35 |
|
ovex |
โข ( ๐ถ Func ๐ท ) โ V |
36 |
35 35
|
mpoex |
โข ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) โ V |
37 |
33 34 36
|
ovmpoa |
โข ( ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ๐ถ Nat ๐ท ) = ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) ) |
38 |
34
|
mpondm0 |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ๐ถ Nat ๐ท ) = โ
) |
39 |
|
funcrcl |
โข ( ๐ โ ( ๐ถ Func ๐ท ) โ ( ๐ถ โ Cat โง ๐ท โ Cat ) ) |
40 |
39
|
con3i |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ยฌ ๐ โ ( ๐ถ Func ๐ท ) ) |
41 |
40
|
eq0rdv |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ๐ถ Func ๐ท ) = โ
) |
42 |
41
|
olcd |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ( ๐ถ Func ๐ท ) = โ
โจ ( ๐ถ Func ๐ท ) = โ
) ) |
43 |
|
0mpo0 |
โข ( ( ( ๐ถ Func ๐ท ) = โ
โจ ( ๐ถ Func ๐ท ) = โ
) โ ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) = โ
) |
44 |
42 43
|
syl |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) = โ
) |
45 |
38 44
|
eqtr4d |
โข ( ยฌ ( ๐ถ โ Cat โง ๐ท โ Cat ) โ ( ๐ถ Nat ๐ท ) = ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) ) |
46 |
37 45
|
pm2.61i |
โข ( ๐ถ Nat ๐ท ) = ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) |
47 |
1 46
|
eqtri |
โข ๐ = ( ๐ โ ( ๐ถ Func ๐ท ) , ๐ โ ( ๐ถ Func ๐ท ) โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ โฆ ( 1st โ ๐ ) / ๐ โฆ { ๐ โ X ๐ฅ โ ๐ต ( ( ๐ โ ๐ฅ ) ๐ฝ ( ๐ โ ๐ฅ ) ) โฃ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ โ โ ( ๐ฅ ๐ป ๐ฆ ) ( ( ๐ โ ๐ฆ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฆ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ) = ( ( ( ๐ฅ ( 2nd โ ๐ ) ๐ฆ ) โ โ ) ( โจ ( ๐ โ ๐ฅ ) , ( ๐ โ ๐ฅ ) โฉ ยท ( ๐ โ ๐ฆ ) ) ( ๐ โ ๐ฅ ) ) } ) |