Step | Hyp | Ref
| Expression |
1 | | fucco.q |
. . . 4
โข ๐ = (๐ถ FuncCat ๐ท) |
2 | | eqid 2737 |
. . . 4
โข (๐ถ Func ๐ท) = (๐ถ Func ๐ท) |
3 | | fucco.n |
. . . 4
โข ๐ = (๐ถ Nat ๐ท) |
4 | | fucco.a |
. . . 4
โข ๐ด = (Baseโ๐ถ) |
5 | | fucco.o |
. . . 4
โข ยท =
(compโ๐ท) |
6 | | fucco.f |
. . . . . . . 8
โข (๐ โ ๐
โ (๐น๐๐บ)) |
7 | 3 | natrcl 17797 |
. . . . . . . 8
โข (๐
โ (๐น๐๐บ) โ (๐น โ (๐ถ Func ๐ท) โง ๐บ โ (๐ถ Func ๐ท))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
โข (๐ โ (๐น โ (๐ถ Func ๐ท) โง ๐บ โ (๐ถ Func ๐ท))) |
9 | 8 | simpld 495 |
. . . . . 6
โข (๐ โ ๐น โ (๐ถ Func ๐ท)) |
10 | | funcrcl 17709 |
. . . . . 6
โข (๐น โ (๐ถ Func ๐ท) โ (๐ถ โ Cat โง ๐ท โ Cat)) |
11 | 9, 10 | syl 17 |
. . . . 5
โข (๐ โ (๐ถ โ Cat โง ๐ท โ Cat)) |
12 | 11 | simpld 495 |
. . . 4
โข (๐ โ ๐ถ โ Cat) |
13 | 11 | simprd 496 |
. . . 4
โข (๐ โ ๐ท โ Cat) |
14 | | fucco.x |
. . . 4
โข โ =
(compโ๐) |
15 | 1, 2, 3, 4, 5, 12,
13, 14 | fuccofval 17807 |
. . 3
โข (๐ โ โ = (๐ฃ โ ((๐ถ Func ๐ท) ร (๐ถ Func ๐ท)), โ โ (๐ถ Func ๐ท) โฆ โฆ(1st
โ๐ฃ) / ๐โฆโฆ(2nd
โ๐ฃ) / ๐โฆ(๐ โ (๐๐โ), ๐ โ (๐๐๐) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ)))))) |
16 | | fvexd 6854 |
. . . 4
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ (1st โ๐ฃ) โ V) |
17 | | simprl 769 |
. . . . . 6
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ ๐ฃ = โจ๐น, ๐บโฉ) |
18 | 17 | fveq2d 6843 |
. . . . 5
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ (1st โ๐ฃ) = (1st
โโจ๐น, ๐บโฉ)) |
19 | | op1stg 7925 |
. . . . . . 7
โข ((๐น โ (๐ถ Func ๐ท) โง ๐บ โ (๐ถ Func ๐ท)) โ (1st โโจ๐น, ๐บโฉ) = ๐น) |
20 | 8, 19 | syl 17 |
. . . . . 6
โข (๐ โ (1st
โโจ๐น, ๐บโฉ) = ๐น) |
21 | 20 | adantr 481 |
. . . . 5
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ (1st โโจ๐น, ๐บโฉ) = ๐น) |
22 | 18, 21 | eqtrd 2777 |
. . . 4
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ (1st โ๐ฃ) = ๐น) |
23 | | fvexd 6854 |
. . . . 5
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ (2nd โ๐ฃ) โ V) |
24 | 17 | adantr 481 |
. . . . . . 7
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ ๐ฃ = โจ๐น, ๐บโฉ) |
25 | 24 | fveq2d 6843 |
. . . . . 6
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ (2nd โ๐ฃ) = (2nd
โโจ๐น, ๐บโฉ)) |
26 | | op2ndg 7926 |
. . . . . . . 8
โข ((๐น โ (๐ถ Func ๐ท) โง ๐บ โ (๐ถ Func ๐ท)) โ (2nd โโจ๐น, ๐บโฉ) = ๐บ) |
27 | 8, 26 | syl 17 |
. . . . . . 7
โข (๐ โ (2nd
โโจ๐น, ๐บโฉ) = ๐บ) |
28 | 27 | ad2antrr 724 |
. . . . . 6
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ (2nd โโจ๐น, ๐บโฉ) = ๐บ) |
29 | 25, 28 | eqtrd 2777 |
. . . . 5
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ (2nd โ๐ฃ) = ๐บ) |
30 | | simpr 485 |
. . . . . . 7
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ = ๐บ) |
31 | | simprr 771 |
. . . . . . . 8
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ โ = ๐ป) |
32 | 31 | ad2antrr 724 |
. . . . . . 7
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ โ = ๐ป) |
33 | 30, 32 | oveq12d 7369 |
. . . . . 6
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐๐โ) = (๐บ๐๐ป)) |
34 | | simplr 767 |
. . . . . . 7
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ = ๐น) |
35 | 34, 30 | oveq12d 7369 |
. . . . . 6
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐๐๐) = (๐น๐๐บ)) |
36 | 34 | fveq2d 6843 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (1st โ๐) = (1st โ๐น)) |
37 | 36 | fveq1d 6841 |
. . . . . . . . . 10
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โ๐)โ๐ฅ) = ((1st โ๐น)โ๐ฅ)) |
38 | 30 | fveq2d 6843 |
. . . . . . . . . . 11
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (1st โ๐) = (1st โ๐บ)) |
39 | 38 | fveq1d 6841 |
. . . . . . . . . 10
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โ๐)โ๐ฅ) = ((1st โ๐บ)โ๐ฅ)) |
40 | 37, 39 | opeq12d 4836 |
. . . . . . . . 9
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ = โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ) |
41 | 32 | fveq2d 6843 |
. . . . . . . . . 10
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (1st โโ) = (1st โ๐ป)) |
42 | 41 | fveq1d 6841 |
. . . . . . . . 9
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โโ)โ๐ฅ) = ((1st โ๐ป)โ๐ฅ)) |
43 | 40, 42 | oveq12d 7369 |
. . . . . . . 8
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (โจ((1st
โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ)) = (โจ((1st
โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))) |
44 | 43 | oveqd 7368 |
. . . . . . 7
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ)) = ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))) |
45 | 44 | mpteq2dv 5205 |
. . . . . 6
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ))) = (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ)))) |
46 | 33, 35, 45 | mpoeq123dv 7426 |
. . . . 5
โข ((((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐ โ (๐๐โ), ๐ โ (๐๐๐) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ)))) = (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))))) |
47 | 23, 29, 46 | csbied2 3893 |
. . . 4
โข (((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โง ๐ = ๐น) โ โฆ(2nd
โ๐ฃ) / ๐โฆ(๐ โ (๐๐โ), ๐ โ (๐๐๐) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ)))) = (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))))) |
48 | 16, 22, 47 | csbied2 3893 |
. . 3
โข ((๐ โง (๐ฃ = โจ๐น, ๐บโฉ โง โ = ๐ป)) โ โฆ(1st
โ๐ฃ) / ๐โฆโฆ(2nd
โ๐ฃ) / ๐โฆ(๐ โ (๐๐โ), ๐ โ (๐๐๐) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐)โ๐ฅ), ((1st โ๐)โ๐ฅ)โฉ ยท ((1st
โโ)โ๐ฅ))(๐โ๐ฅ)))) = (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))))) |
49 | | opelxpi 5668 |
. . . 4
โข ((๐น โ (๐ถ Func ๐ท) โง ๐บ โ (๐ถ Func ๐ท)) โ โจ๐น, ๐บโฉ โ ((๐ถ Func ๐ท) ร (๐ถ Func ๐ท))) |
50 | 8, 49 | syl 17 |
. . 3
โข (๐ โ โจ๐น, ๐บโฉ โ ((๐ถ Func ๐ท) ร (๐ถ Func ๐ท))) |
51 | | fucco.g |
. . . . 5
โข (๐ โ ๐ โ (๐บ๐๐ป)) |
52 | 3 | natrcl 17797 |
. . . . 5
โข (๐ โ (๐บ๐๐ป) โ (๐บ โ (๐ถ Func ๐ท) โง ๐ป โ (๐ถ Func ๐ท))) |
53 | 51, 52 | syl 17 |
. . . 4
โข (๐ โ (๐บ โ (๐ถ Func ๐ท) โง ๐ป โ (๐ถ Func ๐ท))) |
54 | 53 | simprd 496 |
. . 3
โข (๐ โ ๐ป โ (๐ถ Func ๐ท)) |
55 | | ovex 7384 |
. . . . 5
โข (๐บ๐๐ป) โ V |
56 | | ovex 7384 |
. . . . 5
โข (๐น๐๐บ) โ V |
57 | 55, 56 | mpoex 8004 |
. . . 4
โข (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ)))) โ V |
58 | 57 | a1i 11 |
. . 3
โข (๐ โ (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ)))) โ V) |
59 | 15, 48, 50, 54, 58 | ovmpod 7501 |
. 2
โข (๐ โ (โจ๐น, ๐บโฉ โ ๐ป) = (๐ โ (๐บ๐๐ป), ๐ โ (๐น๐๐บ) โฆ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))))) |
60 | | simprl 769 |
. . . . 5
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ ๐ = ๐) |
61 | 60 | fveq1d 6841 |
. . . 4
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ (๐โ๐ฅ) = (๐โ๐ฅ)) |
62 | | simprr 771 |
. . . . 5
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ ๐ = ๐
) |
63 | 62 | fveq1d 6841 |
. . . 4
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ (๐โ๐ฅ) = (๐
โ๐ฅ)) |
64 | 61, 63 | oveq12d 7369 |
. . 3
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ)) = ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐
โ๐ฅ))) |
65 | 64 | mpteq2dv 5205 |
. 2
โข ((๐ โง (๐ = ๐ โง ๐ = ๐
)) โ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐โ๐ฅ))) = (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐
โ๐ฅ)))) |
66 | 4 | fvexi 6853 |
. . . 4
โข ๐ด โ V |
67 | 66 | mptex 7169 |
. . 3
โข (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐
โ๐ฅ))) โ V |
68 | 67 | a1i 11 |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐
โ๐ฅ))) โ V) |
69 | 59, 65, 51, 6, 68 | ovmpod 7501 |
1
โข (๐ โ (๐(โจ๐น, ๐บโฉ โ ๐ป)๐
) = (๐ฅ โ ๐ด โฆ ((๐โ๐ฅ)(โจ((1st โ๐น)โ๐ฅ), ((1st โ๐บ)โ๐ฅ)โฉ ยท ((1st
โ๐ป)โ๐ฅ))(๐
โ๐ฅ)))) |