Step | Hyp | Ref
| Expression |
1 | | evlfcl.e |
. . . . 5
β’ πΈ = (πΆ evalF π·) |
2 | | evlfcl.c |
. . . . 5
β’ (π β πΆ β Cat) |
3 | | evlfcl.d |
. . . . 5
β’ (π β π· β Cat) |
4 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | | eqid 2733 |
. . . . 5
β’
(compβπ·) =
(compβπ·) |
7 | | eqid 2733 |
. . . . 5
β’ (πΆ Nat π·) = (πΆ Nat π·) |
8 | 1, 2, 3, 4, 5, 6, 7 | evlfval 18111 |
. . . 4
β’ (π β πΈ = β¨(π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)), (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β©) |
9 | | ovex 7391 |
. . . . . 6
β’ (πΆ Func π·) β V |
10 | | fvex 6856 |
. . . . . 6
β’
(BaseβπΆ)
β V |
11 | 9, 10 | mpoex 8013 |
. . . . 5
β’ (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)) β V |
12 | 9, 10 | xpex 7688 |
. . . . . 6
β’ ((πΆ Func π·) Γ (BaseβπΆ)) β V |
13 | 12, 12 | mpoex 8013 |
. . . . 5
β’ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ)))) β V |
14 | 11, 13 | opelvv 5673 |
. . . 4
β’
β¨(π β
(πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)), (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β© β (V Γ
V) |
15 | 8, 14 | eqeltrdi 2842 |
. . 3
β’ (π β πΈ β (V Γ V)) |
16 | | 1st2nd2 7961 |
. . 3
β’ (πΈ β (V Γ V) β
πΈ = β¨(1st
βπΈ), (2nd
βπΈ)β©) |
17 | 15, 16 | syl 17 |
. 2
β’ (π β πΈ = β¨(1st βπΈ), (2nd βπΈ)β©) |
18 | | eqid 2733 |
. . . . 5
β’ (π Γc
πΆ) = (π Γc πΆ) |
19 | | evlfcl.q |
. . . . . 6
β’ π = (πΆ FuncCat π·) |
20 | 19 | fucbas 17853 |
. . . . 5
β’ (πΆ Func π·) = (Baseβπ) |
21 | 18, 20, 4 | xpcbas 18071 |
. . . 4
β’ ((πΆ Func π·) Γ (BaseβπΆ)) = (Baseβ(π Γc πΆ)) |
22 | | eqid 2733 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
23 | | eqid 2733 |
. . . 4
β’ (Hom
β(π
Γc πΆ)) = (Hom β(π Γc πΆ)) |
24 | | eqid 2733 |
. . . 4
β’ (Hom
βπ·) = (Hom
βπ·) |
25 | | eqid 2733 |
. . . 4
β’
(Idβ(π
Γc πΆ)) = (Idβ(π Γc πΆ)) |
26 | | eqid 2733 |
. . . 4
β’
(Idβπ·) =
(Idβπ·) |
27 | | eqid 2733 |
. . . 4
β’
(compβ(π
Γc πΆ)) = (compβ(π Γc πΆ)) |
28 | 19, 2, 3 | fuccat 17864 |
. . . . 5
β’ (π β π β Cat) |
29 | 18, 28, 2 | xpccat 18083 |
. . . 4
β’ (π β (π Γc πΆ) β Cat) |
30 | | relfunc 17753 |
. . . . . . . . . . 11
β’ Rel
(πΆ Func π·) |
31 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (πΆ Func π·)) β π β (πΆ Func π·)) |
32 | | 1st2ndbr 7975 |
. . . . . . . . . . 11
β’ ((Rel
(πΆ Func π·) β§ π β (πΆ Func π·)) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
33 | 30, 31, 32 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ π β (πΆ Func π·)) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
34 | 4, 22, 33 | funcf1 17757 |
. . . . . . . . 9
β’ ((π β§ π β (πΆ Func π·)) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
35 | 34 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ π β (πΆ Func π·)) β§ π₯ β (BaseβπΆ)) β ((1st βπ)βπ₯) β (Baseβπ·)) |
36 | 35 | ralrimiva 3140 |
. . . . . . 7
β’ ((π β§ π β (πΆ Func π·)) β βπ₯ β (BaseβπΆ)((1st βπ)βπ₯) β (Baseβπ·)) |
37 | 36 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β (πΆ Func π·)βπ₯ β (BaseβπΆ)((1st βπ)βπ₯) β (Baseβπ·)) |
38 | | eqid 2733 |
. . . . . . 7
β’ (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)) = (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)) |
39 | 38 | fmpo 8001 |
. . . . . 6
β’
(βπ β
(πΆ Func π·)βπ₯ β (BaseβπΆ)((1st βπ)βπ₯) β (Baseβπ·) β (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)):((πΆ Func π·) Γ (BaseβπΆ))βΆ(Baseβπ·)) |
40 | 37, 39 | sylib 217 |
. . . . 5
β’ (π β (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)):((πΆ Func π·) Γ (BaseβπΆ))βΆ(Baseβπ·)) |
41 | 11, 13 | op1std 7932 |
. . . . . . 7
β’ (πΈ = β¨(π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)), (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β© β (1st
βπΈ) = (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯))) |
42 | 8, 41 | syl 17 |
. . . . . 6
β’ (π β (1st
βπΈ) = (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯))) |
43 | 42 | feq1d 6654 |
. . . . 5
β’ (π β ((1st
βπΈ):((πΆ Func π·) Γ (BaseβπΆ))βΆ(Baseβπ·) β (π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)):((πΆ Func π·) Γ (BaseβπΆ))βΆ(Baseβπ·))) |
44 | 40, 43 | mpbird 257 |
. . . 4
β’ (π β (1st
βπΈ):((πΆ Func π·) Γ (BaseβπΆ))βΆ(Baseβπ·)) |
45 | | eqid 2733 |
. . . . . 6
β’ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ)))) = (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ)))) |
46 | | ovex 7391 |
. . . . . . . . 9
β’ (π(πΆ Nat π·)π) β V |
47 | | ovex 7391 |
. . . . . . . . 9
β’
((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β V |
48 | 46, 47 | mpoex 8013 |
. . . . . . . 8
β’ (π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))) β V |
49 | 48 | csbex 5269 |
. . . . . . 7
β’
β¦(1st βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))) β V |
50 | 49 | csbex 5269 |
. . . . . 6
β’
β¦(1st βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))) β V |
51 | 45, 50 | fnmpoi 8003 |
. . . . 5
β’ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ)))) Fn (((πΆ Func π·) Γ (BaseβπΆ)) Γ ((πΆ Func π·) Γ (BaseβπΆ))) |
52 | 11, 13 | op2ndd 7933 |
. . . . . . 7
β’ (πΈ = β¨(π β (πΆ Func π·), π₯ β (BaseβπΆ) β¦ ((1st βπ)βπ₯)), (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))β© β (2nd
βπΈ) = (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))) |
53 | 8, 52 | syl 17 |
. . . . . 6
β’ (π β (2nd
βπΈ) = (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ))))) |
54 | 53 | fneq1d 6596 |
. . . . 5
β’ (π β ((2nd
βπΈ) Fn (((πΆ Func π·) Γ (BaseβπΆ)) Γ ((πΆ Func π·) Γ (BaseβπΆ))) β (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)), π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β¦ β¦(1st
βπ₯) / πβ¦β¦(1st
βπ¦) / πβ¦(π β (π(πΆ Nat π·)π), π β ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)) β¦ ((πβ(2nd βπ¦))(β¨((1st
βπ)β(2nd βπ₯)), ((1st
βπ)β(2nd βπ¦))β©(compβπ·)((1st βπ)β(2nd
βπ¦)))(((2nd βπ₯)(2nd βπ)(2nd βπ¦))βπ)))) Fn (((πΆ Func π·) Γ (BaseβπΆ)) Γ ((πΆ Func π·) Γ (BaseβπΆ))))) |
55 | 51, 54 | mpbiri 258 |
. . . 4
β’ (π β (2nd
βπΈ) Fn (((πΆ Func π·) Γ (BaseβπΆ)) Γ ((πΆ Func π·) Γ (BaseβπΆ)))) |
56 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β π· β Cat) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β π· β Cat) |
58 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β π β (πΆ Func π·)) |
59 | 30, 58, 32 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
60 | 4, 22, 59 | funcf1 17757 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
62 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β π’ β (BaseβπΆ)) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β π’ β (BaseβπΆ)) |
64 | 61, 63 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β ((1st βπ)βπ’) β (Baseβπ·)) |
65 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β π£ β (BaseβπΆ)) |
66 | 61, 65 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β ((1st βπ)βπ£) β (Baseβπ·)) |
67 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β π β (πΆ Func π·)) |
68 | | 1st2ndbr 7975 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Rel
(πΆ Func π·) β§ π β (πΆ Func π·)) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
69 | 30, 67, 68 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
70 | 4, 22, 69 | funcf1 17757 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
72 | 71, 65 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β ((1st βπ)βπ£) β (Baseβπ·)) |
73 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β π£ β (BaseβπΆ)) |
74 | 4, 5, 24, 59, 62, 73 | funcf2 17759 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (π’(2nd βπ)π£):(π’(Hom βπΆ)π£)βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β (π’(2nd βπ)π£):(π’(Hom βπΆ)π£)βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
76 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β β β (π’(Hom βπΆ)π£)) |
77 | 75, 76 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β ((π’(2nd βπ)π£)ββ) β (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
78 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β π β (π(πΆ Nat π·)π)) |
79 | 7, 78 | nat1st2nd 17843 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β π β (β¨(1st βπ), (2nd βπ)β©(πΆ Nat π·)β¨(1st βπ), (2nd βπ)β©)) |
80 | 7, 79, 4, 24, 65 | natcl 17845 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β (πβπ£) β (((1st βπ)βπ£)(Hom βπ·)((1st βπ)βπ£))) |
81 | 22, 24, 6, 57, 64, 66, 72, 77, 80 | catcocl 17570 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β§ (π β (π(πΆ Nat π·)π) β§ β β (π’(Hom βπΆ)π£))) β ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ)) β (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
82 | 81 | ralrimivva 3194 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β βπ β (π(πΆ Nat π·)π)ββ β (π’(Hom βπΆ)π£)((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ)) β (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
83 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ))) = (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ))) |
84 | 83 | fmpo 8001 |
. . . . . . . . . . . . 13
β’
(βπ β
(π(πΆ Nat π·)π)ββ β (π’(Hom βπΆ)π£)((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ)) β (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£)) β (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ))):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
85 | 82, 84 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ))):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
86 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β πΆ β Cat) |
87 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(β¨π, π’β©(2nd
βπΈ)β¨π, π£β©) = (β¨π, π’β©(2nd βπΈ)β¨π, π£β©) |
88 | 1, 86, 56, 4, 5, 6,
7, 58, 67, 62, 73, 87 | evlf2 18112 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (β¨π, π’β©(2nd βπΈ)β¨π, π£β©) = (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ)))) |
89 | 88 | feq1d 6654 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β ((β¨π, π’β©(2nd βπΈ)β¨π, π£β©):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£)) β (π β (π(πΆ Nat π·)π), β β (π’(Hom βπΆ)π£) β¦ ((πβπ£)(β¨((1st βπ)βπ’), ((1st βπ)βπ£)β©(compβπ·)((1st βπ)βπ£))((π’(2nd βπ)π£)ββ))):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£)))) |
90 | 85, 89 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (β¨π, π’β©(2nd βπΈ)β¨π, π£β©):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
91 | 19, 7 | fuchom 17854 |
. . . . . . . . . . . . 13
β’ (πΆ Nat π·) = (Hom βπ) |
92 | 18, 20, 4, 91, 5, 58, 62, 67, 73, 23 | xpchom2 18079 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©) = ((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))) |
93 | 1, 86, 56, 4, 58, 62 | evlf1 18114 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (π(1st βπΈ)π’) = ((1st βπ)βπ’)) |
94 | 1, 86, 56, 4, 67, 73 | evlf1 18114 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (π(1st βπΈ)π£) = ((1st βπ)βπ£)) |
95 | 93, 94 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£)) = (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£))) |
96 | 92, 95 | feq23d 6664 |
. . . . . . . . . . 11
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β ((β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£)) β (β¨π, π’β©(2nd βπΈ)β¨π, π£β©):((π(πΆ Nat π·)π) Γ (π’(Hom βπΆ)π£))βΆ(((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ£)))) |
97 | 90, 96 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β§ (π β (πΆ Func π·) β§ π£ β (BaseβπΆ))) β (β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£))) |
98 | 97 | ralrimivva 3194 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£))) |
99 | 98 | ralrimivva 3194 |
. . . . . . . 8
β’ (π β βπ β (πΆ Func π·)βπ’ β (BaseβπΆ)βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£))) |
100 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = β¨π, π£β© β (π₯(2nd βπΈ)π¦) = (π₯(2nd βπΈ)β¨π, π£β©)) |
101 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = β¨π, π£β© β (π₯(Hom β(π Γc πΆ))π¦) = (π₯(Hom β(π Γc πΆ))β¨π, π£β©)) |
102 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π¦ = β¨π, π£β© β ((1st βπΈ)βπ¦) = ((1st βπΈ)ββ¨π, π£β©)) |
103 | | df-ov 7361 |
. . . . . . . . . . . . . 14
β’ (π(1st βπΈ)π£) = ((1st βπΈ)ββ¨π, π£β©) |
104 | 102, 103 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π¦ = β¨π, π£β© β ((1st βπΈ)βπ¦) = (π(1st βπΈ)π£)) |
105 | 104 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π¦ = β¨π, π£β© β (((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦)) = (((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£))) |
106 | 100, 101,
105 | feq123d 6658 |
. . . . . . . . . . 11
β’ (π¦ = β¨π, π£β© β ((π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦)) β (π₯(2nd βπΈ)β¨π, π£β©):(π₯(Hom β(π Γc πΆ))β¨π, π£β©)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£)))) |
107 | 106 | ralxp 5798 |
. . . . . . . . . 10
β’
(βπ¦ β
((πΆ Func π·) Γ (BaseβπΆ))(π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦)) β βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(π₯(2nd βπΈ)β¨π, π£β©):(π₯(Hom β(π Γc πΆ))β¨π, π£β©)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£))) |
108 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = β¨π, π’β© β (π₯(2nd βπΈ)β¨π, π£β©) = (β¨π, π’β©(2nd βπΈ)β¨π, π£β©)) |
109 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = β¨π, π’β© β (π₯(Hom β(π Γc πΆ))β¨π, π£β©) = (β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)) |
110 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = β¨π, π’β© β ((1st βπΈ)βπ₯) = ((1st βπΈ)ββ¨π, π’β©)) |
111 | | df-ov 7361 |
. . . . . . . . . . . . . 14
β’ (π(1st βπΈ)π’) = ((1st βπΈ)ββ¨π, π’β©) |
112 | 110, 111 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π₯ = β¨π, π’β© β ((1st βπΈ)βπ₯) = (π(1st βπΈ)π’)) |
113 | 112 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π₯ = β¨π, π’β© β (((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£)) = ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£))) |
114 | 108, 109,
113 | feq123d 6658 |
. . . . . . . . . . 11
β’ (π₯ = β¨π, π’β© β ((π₯(2nd βπΈ)β¨π, π£β©):(π₯(Hom β(π Γc πΆ))β¨π, π£β©)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£)) β (β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£)))) |
115 | 114 | 2ralbidv 3209 |
. . . . . . . . . 10
β’ (π₯ = β¨π, π’β© β (βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(π₯(2nd βπΈ)β¨π, π£β©):(π₯(Hom β(π Γc πΆ))β¨π, π£β©)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)(π(1st βπΈ)π£)) β βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£)))) |
116 | 107, 115 | bitrid 283 |
. . . . . . . . 9
β’ (π₯ = β¨π, π’β© β (βπ¦ β ((πΆ Func π·) Γ (BaseβπΆ))(π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦)) β βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£)))) |
117 | 116 | ralxp 5798 |
. . . . . . . 8
β’
(βπ₯ β
((πΆ Func π·) Γ (BaseβπΆ))βπ¦ β ((πΆ Func π·) Γ (BaseβπΆ))(π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦)) β βπ β (πΆ Func π·)βπ’ β (BaseβπΆ)βπ β (πΆ Func π·)βπ£ β (BaseβπΆ)(β¨π, π’β©(2nd βπΈ)β¨π, π£β©):(β¨π, π’β©(Hom β(π Γc πΆ))β¨π, π£β©)βΆ((π(1st βπΈ)π’)(Hom βπ·)(π(1st βπΈ)π£))) |
118 | 99, 117 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β ((πΆ Func π·) Γ (BaseβπΆ))βπ¦ β ((πΆ Func π·) Γ (BaseβπΆ))(π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦))) |
119 | 118 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π₯ β ((πΆ Func π·) Γ (BaseβπΆ))) β βπ¦ β ((πΆ Func π·) Γ (BaseβπΆ))(π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦))) |
120 | 119 | r19.21bi 3233 |
. . . . 5
β’ (((π β§ π₯ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ))) β (π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦))) |
121 | 120 | anasss 468 |
. . . 4
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)))) β (π₯(2nd βπΈ)π¦):(π₯(Hom β(π Γc πΆ))π¦)βΆ(((1st βπΈ)βπ₯)(Hom βπ·)((1st βπΈ)βπ¦))) |
122 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β π β Cat) |
123 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β πΆ β Cat) |
124 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Idβπ) =
(Idβπ) |
125 | | eqid 2733 |
. . . . . . . . . . 11
β’
(IdβπΆ) =
(IdβπΆ) |
126 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β π β (πΆ Func π·)) |
127 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β π’ β (BaseβπΆ)) |
128 | 18, 122, 123, 20, 4, 124, 125, 25, 126, 127 | xpcid 18082 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((Idβ(π Γc πΆ))ββ¨π, π’β©) = β¨((Idβπ)βπ), ((IdβπΆ)βπ’)β©) |
129 | 128 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)ββ¨((Idβπ)βπ), ((IdβπΆ)βπ’)β©)) |
130 | | df-ov 7361 |
. . . . . . . . 9
β’
(((Idβπ)βπ)(β¨π, π’β©(2nd βπΈ)β¨π, π’β©)((IdβπΆ)βπ’)) = ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)ββ¨((Idβπ)βπ), ((IdβπΆ)βπ’)β©) |
131 | 129, 130 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = (((Idβπ)βπ)(β¨π, π’β©(2nd βπΈ)β¨π, π’β©)((IdβπΆ)βπ’))) |
132 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β π· β Cat) |
133 | | eqid 2733 |
. . . . . . . . 9
β’
(β¨π, π’β©(2nd
βπΈ)β¨π, π’β©) = (β¨π, π’β©(2nd βπΈ)β¨π, π’β©) |
134 | 20, 91, 124, 122, 126 | catidcl 17567 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((Idβπ)βπ) β (π(πΆ Nat π·)π)) |
135 | 4, 5, 125, 123, 127 | catidcl 17567 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((IdβπΆ)βπ’) β (π’(Hom βπΆ)π’)) |
136 | 1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135 | evlf2val 18113 |
. . . . . . . 8
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (((Idβπ)βπ)(β¨π, π’β©(2nd βπΈ)β¨π, π’β©)((IdβπΆ)βπ’)) = ((((Idβπ)βπ)βπ’)(β¨((1st βπ)βπ’), ((1st βπ)βπ’)β©(compβπ·)((1st βπ)βπ’))((π’(2nd βπ)π’)β((IdβπΆ)βπ’)))) |
137 | 30, 126, 32 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (1st βπ)(πΆ Func π·)(2nd βπ)) |
138 | 4, 22, 137 | funcf1 17757 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (1st βπ):(BaseβπΆ)βΆ(Baseβπ·)) |
139 | 138, 127 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((1st βπ)βπ’) β (Baseβπ·)) |
140 | 22, 24, 26, 132, 139 | catidcl 17567 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((Idβπ·)β((1st βπ)βπ’)) β (((1st βπ)βπ’)(Hom βπ·)((1st βπ)βπ’))) |
141 | 22, 24, 26, 132, 139, 6, 139, 140 | catlid 17568 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (((Idβπ·)β((1st βπ)βπ’))(β¨((1st βπ)βπ’), ((1st βπ)βπ’)β©(compβπ·)((1st βπ)βπ’))((Idβπ·)β((1st βπ)βπ’))) = ((Idβπ·)β((1st βπ)βπ’))) |
142 | 19, 124, 26, 126 | fucid 17865 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((Idβπ)βπ) = ((Idβπ·) β (1st βπ))) |
143 | 142 | fveq1d 6845 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (((Idβπ)βπ)βπ’) = (((Idβπ·) β (1st βπ))βπ’)) |
144 | | fvco3 6941 |
. . . . . . . . . . . 12
β’
(((1st βπ):(BaseβπΆ)βΆ(Baseβπ·) β§ π’ β (BaseβπΆ)) β (((Idβπ·) β (1st βπ))βπ’) = ((Idβπ·)β((1st βπ)βπ’))) |
145 | 138, 127,
144 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (((Idβπ·) β (1st βπ))βπ’) = ((Idβπ·)β((1st βπ)βπ’))) |
146 | 143, 145 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (((Idβπ)βπ)βπ’) = ((Idβπ·)β((1st βπ)βπ’))) |
147 | 4, 125, 26, 137, 127 | funcid 17761 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((π’(2nd βπ)π’)β((IdβπΆ)βπ’)) = ((Idβπ·)β((1st βπ)βπ’))) |
148 | 146, 147 | oveq12d 7376 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((((Idβπ)βπ)βπ’)(β¨((1st βπ)βπ’), ((1st βπ)βπ’)β©(compβπ·)((1st βπ)βπ’))((π’(2nd βπ)π’)β((IdβπΆ)βπ’))) = (((Idβπ·)β((1st βπ)βπ’))(β¨((1st βπ)βπ’), ((1st βπ)βπ’)β©(compβπ·)((1st βπ)βπ’))((Idβπ·)β((1st βπ)βπ’)))) |
149 | 1, 123, 132, 4, 126, 127 | evlf1 18114 |
. . . . . . . . . 10
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β (π(1st βπΈ)π’) = ((1st βπ)βπ’)) |
150 | 149 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((Idβπ·)β(π(1st βπΈ)π’)) = ((Idβπ·)β((1st βπ)βπ’))) |
151 | 141, 148,
150 | 3eqtr4d 2783 |
. . . . . . . 8
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((((Idβπ)βπ)βπ’)(β¨((1st βπ)βπ’), ((1st βπ)βπ’)β©(compβπ·)((1st βπ)βπ’))((π’(2nd βπ)π’)β((IdβπΆ)βπ’))) = ((Idβπ·)β(π(1st βπΈ)π’))) |
152 | 131, 136,
151 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π β§ (π β (πΆ Func π·) β§ π’ β (BaseβπΆ))) β ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = ((Idβπ·)β(π(1st βπΈ)π’))) |
153 | 152 | ralrimivva 3194 |
. . . . . 6
β’ (π β βπ β (πΆ Func π·)βπ’ β (BaseβπΆ)((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = ((Idβπ·)β(π(1st βπΈ)π’))) |
154 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = β¨π, π’β© β π₯ = β¨π, π’β©) |
155 | 154, 154 | oveq12d 7376 |
. . . . . . . . 9
β’ (π₯ = β¨π, π’β© β (π₯(2nd βπΈ)π₯) = (β¨π, π’β©(2nd βπΈ)β¨π, π’β©)) |
156 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = β¨π, π’β© β ((Idβ(π Γc πΆ))βπ₯) = ((Idβ(π Γc πΆ))ββ¨π, π’β©)) |
157 | 155, 156 | fveq12d 6850 |
. . . . . . . 8
β’ (π₯ = β¨π, π’β© β ((π₯(2nd βπΈ)π₯)β((Idβ(π Γc πΆ))βπ₯)) = ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©))) |
158 | 112 | fveq2d 6847 |
. . . . . . . 8
β’ (π₯ = β¨π, π’β© β ((Idβπ·)β((1st βπΈ)βπ₯)) = ((Idβπ·)β(π(1st βπΈ)π’))) |
159 | 157, 158 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = β¨π, π’β© β (((π₯(2nd βπΈ)π₯)β((Idβ(π Γc πΆ))βπ₯)) = ((Idβπ·)β((1st βπΈ)βπ₯)) β ((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = ((Idβπ·)β(π(1st βπΈ)π’)))) |
160 | 159 | ralxp 5798 |
. . . . . 6
β’
(βπ₯ β
((πΆ Func π·) Γ (BaseβπΆ))((π₯(2nd βπΈ)π₯)β((Idβ(π Γc πΆ))βπ₯)) = ((Idβπ·)β((1st βπΈ)βπ₯)) β βπ β (πΆ Func π·)βπ’ β (BaseβπΆ)((β¨π, π’β©(2nd βπΈ)β¨π, π’β©)β((Idβ(π Γc πΆ))ββ¨π, π’β©)) = ((Idβπ·)β(π(1st βπΈ)π’))) |
161 | 153, 160 | sylibr 233 |
. . . . 5
β’ (π β βπ₯ β ((πΆ Func π·) Γ (BaseβπΆ))((π₯(2nd βπΈ)π₯)β((Idβ(π Γc πΆ))βπ₯)) = ((Idβπ·)β((1st βπΈ)βπ₯))) |
162 | 161 | r19.21bi 3233 |
. . . 4
β’ ((π β§ π₯ β ((πΆ Func π·) Γ (BaseβπΆ))) β ((π₯(2nd βπΈ)π₯)β((Idβ(π Γc πΆ))βπ₯)) = ((Idβπ·)β((1st βπΈ)βπ₯))) |
163 | 2 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β πΆ β Cat) |
164 | 3 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π· β Cat) |
165 | | simp21 1207 |
. . . . . . . . 9
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π₯ β ((πΆ Func π·) Γ (BaseβπΆ))) |
166 | | 1st2nd2 7961 |
. . . . . . . . 9
β’ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
167 | 165, 166 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
168 | 167, 165 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨(1st βπ₯), (2nd βπ₯)β© β ((πΆ Func π·) Γ (BaseβπΆ))) |
169 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β ((πΆ Func π·) Γ (BaseβπΆ)) β ((1st βπ₯) β (πΆ Func π·) β§ (2nd βπ₯) β (BaseβπΆ))) |
170 | 168, 169 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπ₯) β (πΆ Func π·) β§ (2nd βπ₯) β (BaseβπΆ))) |
171 | | simp22 1208 |
. . . . . . . . 9
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π¦ β ((πΆ Func π·) Γ (BaseβπΆ))) |
172 | | 1st2nd2 7961 |
. . . . . . . . 9
β’ (π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
173 | 171, 172 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
174 | 173, 171 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨(1st βπ¦), (2nd βπ¦)β© β ((πΆ Func π·) Γ (BaseβπΆ))) |
175 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπ¦), (2nd βπ¦)β© β ((πΆ Func π·) Γ (BaseβπΆ)) β ((1st βπ¦) β (πΆ Func π·) β§ (2nd βπ¦) β (BaseβπΆ))) |
176 | 174, 175 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπ¦) β (πΆ Func π·) β§ (2nd βπ¦) β (BaseβπΆ))) |
177 | | simp23 1209 |
. . . . . . . . 9
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π§ β ((πΆ Func π·) Γ (BaseβπΆ))) |
178 | | 1st2nd2 7961 |
. . . . . . . . 9
β’ (π§ β ((πΆ Func π·) Γ (BaseβπΆ)) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
179 | 177, 178 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
180 | 179, 177 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨(1st βπ§), (2nd βπ§)β© β ((πΆ Func π·) Γ (BaseβπΆ))) |
181 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπ§), (2nd βπ§)β© β ((πΆ Func π·) Γ (BaseβπΆ)) β ((1st βπ§) β (πΆ Func π·) β§ (2nd βπ§) β (BaseβπΆ))) |
182 | 180, 181 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπ§) β (πΆ Func π·) β§ (2nd βπ§) β (BaseβπΆ))) |
183 | | simp3l 1202 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π β (π₯(Hom β(π Γc πΆ))π¦)) |
184 | 18, 21, 91, 5, 23, 165, 171 | xpchom 18073 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π₯(Hom β(π Γc πΆ))π¦) = (((1st βπ₯)(πΆ Nat π·)(1st βπ¦)) Γ ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)))) |
185 | 183, 184 | eleqtrd 2836 |
. . . . . . . . 9
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π β (((1st βπ₯)(πΆ Nat π·)(1st βπ¦)) Γ ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)))) |
186 | | 1st2nd2 7961 |
. . . . . . . . 9
β’ (π β (((1st
βπ₯)(πΆ Nat π·)(1st βπ¦)) Γ ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦))) β π = β¨(1st βπ), (2nd βπ)β©) |
187 | 185, 186 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π = β¨(1st βπ), (2nd βπ)β©) |
188 | 187, 185 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨(1st βπ), (2nd βπ)β© β (((1st
βπ₯)(πΆ Nat π·)(1st βπ¦)) Γ ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦)))) |
189 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπ), (2nd βπ)β© β (((1st βπ₯)(πΆ Nat π·)(1st βπ¦)) Γ ((2nd βπ₯)(Hom βπΆ)(2nd βπ¦))) β ((1st βπ) β ((1st
βπ₯)(πΆ Nat π·)(1st βπ¦)) β§ (2nd βπ) β ((2nd
βπ₯)(Hom βπΆ)(2nd βπ¦)))) |
190 | 188, 189 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπ) β ((1st
βπ₯)(πΆ Nat π·)(1st βπ¦)) β§ (2nd βπ) β ((2nd
βπ₯)(Hom βπΆ)(2nd βπ¦)))) |
191 | | simp3r 1203 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π β (π¦(Hom β(π Γc πΆ))π§)) |
192 | 18, 21, 91, 5, 23, 171, 177 | xpchom 18073 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π¦(Hom β(π Γc πΆ))π§) = (((1st βπ¦)(πΆ Nat π·)(1st βπ§)) Γ ((2nd βπ¦)(Hom βπΆ)(2nd βπ§)))) |
193 | 191, 192 | eleqtrd 2836 |
. . . . . . . . 9
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π β (((1st βπ¦)(πΆ Nat π·)(1st βπ§)) Γ ((2nd βπ¦)(Hom βπΆ)(2nd βπ§)))) |
194 | | 1st2nd2 7961 |
. . . . . . . . 9
β’ (π β (((1st
βπ¦)(πΆ Nat π·)(1st βπ§)) Γ ((2nd βπ¦)(Hom βπΆ)(2nd βπ§))) β π = β¨(1st βπ), (2nd βπ)β©) |
195 | 193, 194 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β π = β¨(1st βπ), (2nd βπ)β©) |
196 | 195, 193 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨(1st βπ), (2nd βπ)β© β (((1st
βπ¦)(πΆ Nat π·)(1st βπ§)) Γ ((2nd βπ¦)(Hom βπΆ)(2nd βπ§)))) |
197 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπ), (2nd βπ)β© β (((1st βπ¦)(πΆ Nat π·)(1st βπ§)) Γ ((2nd βπ¦)(Hom βπΆ)(2nd βπ§))) β ((1st βπ) β ((1st
βπ¦)(πΆ Nat π·)(1st βπ§)) β§ (2nd βπ) β ((2nd
βπ¦)(Hom βπΆ)(2nd βπ§)))) |
198 | 196, 197 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπ) β ((1st
βπ¦)(πΆ Nat π·)(1st βπ§)) β§ (2nd βπ) β ((2nd
βπ¦)(Hom βπΆ)(2nd βπ§)))) |
199 | 1, 19, 163, 164, 7, 170, 176, 182, 190, 198 | evlfcllem 18115 |
. . . . 5
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((β¨(1st
βπ₯), (2nd
βπ₯)β©(2nd βπΈ)β¨(1st
βπ§), (2nd
βπ§)β©)β(β¨(1st
βπ), (2nd
βπ)β©(β¨β¨(1st
βπ₯), (2nd
βπ₯)β©,
β¨(1st βπ¦), (2nd βπ¦)β©β©(compβ(π Γc πΆ))β¨(1st
βπ§), (2nd
βπ§)β©)β¨(1st βπ), (2nd βπ)β©)) =
(((β¨(1st βπ¦), (2nd βπ¦)β©(2nd βπΈ)β¨(1st
βπ§), (2nd
βπ§)β©)ββ¨(1st
βπ), (2nd
βπ)β©)(β¨((1st βπΈ)ββ¨(1st
βπ₯), (2nd
βπ₯)β©),
((1st βπΈ)ββ¨(1st βπ¦), (2nd βπ¦)β©)β©(compβπ·)((1st βπΈ)ββ¨(1st
βπ§), (2nd
βπ§)β©))((β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ¦), (2nd βπ¦)β©)ββ¨(1st
βπ), (2nd
βπ)β©))) |
200 | 167, 179 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π₯(2nd βπΈ)π§) = (β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ§), (2nd βπ§)β©)) |
201 | 167, 173 | opeq12d 4839 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨π₯, π¦β© = β¨β¨(1st
βπ₯), (2nd
βπ₯)β©,
β¨(1st βπ¦), (2nd βπ¦)β©β©) |
202 | 201, 179 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (β¨π₯, π¦β©(compβ(π Γc πΆ))π§) = (β¨β¨(1st βπ₯), (2nd βπ₯)β©, β¨(1st
βπ¦), (2nd
βπ¦)β©β©(compβ(π Γc πΆ))β¨(1st
βπ§), (2nd
βπ§)β©)) |
203 | 202, 195,
187 | oveq123d 7379 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π(β¨π₯, π¦β©(compβ(π Γc πΆ))π§)π) = (β¨(1st βπ), (2nd βπ)β©(β¨β¨(1st
βπ₯), (2nd
βπ₯)β©,
β¨(1st βπ¦), (2nd βπ¦)β©β©(compβ(π Γc πΆ))β¨(1st
βπ§), (2nd
βπ§)β©)β¨(1st βπ), (2nd βπ)β©)) |
204 | 200, 203 | fveq12d 6850 |
. . . . 5
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((π₯(2nd βπΈ)π§)β(π(β¨π₯, π¦β©(compβ(π Γc πΆ))π§)π)) = ((β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ§), (2nd βπ§)β©)β(β¨(1st
βπ), (2nd
βπ)β©(β¨β¨(1st
βπ₯), (2nd
βπ₯)β©,
β¨(1st βπ¦), (2nd βπ¦)β©β©(compβ(π Γc πΆ))β¨(1st
βπ§), (2nd
βπ§)β©)β¨(1st βπ), (2nd βπ)β©))) |
205 | 167 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπΈ)βπ₯) = ((1st βπΈ)ββ¨(1st βπ₯), (2nd βπ₯)β©)) |
206 | 173 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπΈ)βπ¦) = ((1st βπΈ)ββ¨(1st βπ¦), (2nd βπ¦)β©)) |
207 | 205, 206 | opeq12d 4839 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β β¨((1st
βπΈ)βπ₯), ((1st βπΈ)βπ¦)β© = β¨((1st βπΈ)ββ¨(1st
βπ₯), (2nd
βπ₯)β©),
((1st βπΈ)ββ¨(1st βπ¦), (2nd βπ¦)β©)β©) |
208 | 179 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((1st βπΈ)βπ§) = ((1st βπΈ)ββ¨(1st βπ§), (2nd βπ§)β©)) |
209 | 207, 208 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (β¨((1st
βπΈ)βπ₯), ((1st βπΈ)βπ¦)β©(compβπ·)((1st βπΈ)βπ§)) = (β¨((1st βπΈ)ββ¨(1st
βπ₯), (2nd
βπ₯)β©),
((1st βπΈ)ββ¨(1st βπ¦), (2nd βπ¦)β©)β©(compβπ·)((1st βπΈ)ββ¨(1st
βπ§), (2nd
βπ§)β©))) |
210 | 173, 179 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π¦(2nd βπΈ)π§) = (β¨(1st βπ¦), (2nd βπ¦)β©(2nd
βπΈ)β¨(1st βπ§), (2nd βπ§)β©)) |
211 | 210, 195 | fveq12d 6850 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((π¦(2nd βπΈ)π§)βπ) = ((β¨(1st βπ¦), (2nd βπ¦)β©(2nd
βπΈ)β¨(1st βπ§), (2nd βπ§)β©)ββ¨(1st
βπ), (2nd
βπ)β©)) |
212 | 167, 173 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (π₯(2nd βπΈ)π¦) = (β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ¦), (2nd βπ¦)β©)) |
213 | 212, 187 | fveq12d 6850 |
. . . . . 6
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((π₯(2nd βπΈ)π¦)βπ) = ((β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ¦), (2nd βπ¦)β©)ββ¨(1st
βπ), (2nd
βπ)β©)) |
214 | 209, 211,
213 | oveq123d 7379 |
. . . . 5
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β (((π¦(2nd βπΈ)π§)βπ)(β¨((1st βπΈ)βπ₯), ((1st βπΈ)βπ¦)β©(compβπ·)((1st βπΈ)βπ§))((π₯(2nd βπΈ)π¦)βπ)) = (((β¨(1st βπ¦), (2nd βπ¦)β©(2nd
βπΈ)β¨(1st βπ§), (2nd βπ§)β©)ββ¨(1st
βπ), (2nd
βπ)β©)(β¨((1st βπΈ)ββ¨(1st
βπ₯), (2nd
βπ₯)β©),
((1st βπΈ)ββ¨(1st βπ¦), (2nd βπ¦)β©)β©(compβπ·)((1st βπΈ)ββ¨(1st
βπ§), (2nd
βπ§)β©))((β¨(1st βπ₯), (2nd βπ₯)β©(2nd
βπΈ)β¨(1st βπ¦), (2nd βπ¦)β©)ββ¨(1st
βπ), (2nd
βπ)β©))) |
215 | 199, 204,
214 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π₯ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π¦ β ((πΆ Func π·) Γ (BaseβπΆ)) β§ π§ β ((πΆ Func π·) Γ (BaseβπΆ))) β§ (π β (π₯(Hom β(π Γc πΆ))π¦) β§ π β (π¦(Hom β(π Γc πΆ))π§))) β ((π₯(2nd βπΈ)π§)β(π(β¨π₯, π¦β©(compβ(π Γc πΆ))π§)π)) = (((π¦(2nd βπΈ)π§)βπ)(β¨((1st βπΈ)βπ₯), ((1st βπΈ)βπ¦)β©(compβπ·)((1st βπΈ)βπ§))((π₯(2nd βπΈ)π¦)βπ))) |
216 | 21, 22, 23, 24, 25, 26, 27, 6, 29, 3, 44, 55, 121, 162, 215 | isfuncd 17756 |
. . 3
β’ (π β (1st
βπΈ)((π Γc
πΆ) Func π·)(2nd βπΈ)) |
217 | | df-br 5107 |
. . 3
β’
((1st βπΈ)((π Γc πΆ) Func π·)(2nd βπΈ) β β¨(1st βπΈ), (2nd βπΈ)β© β ((π Γc
πΆ) Func π·)) |
218 | 216, 217 | sylib 217 |
. 2
β’ (π β β¨(1st
βπΈ), (2nd
βπΈ)β© β
((π
Γc πΆ) Func π·)) |
219 | 17, 218 | eqeltrd 2834 |
1
β’ (π β πΈ β ((π Γc πΆ) Func π·)) |