Step | Hyp | Ref
| Expression |
1 | | catcfuccl.o |
. . . . 5
β’ π = (π FuncCat π) |
2 | | eqid 2733 |
. . . . 5
β’ (π Func π) = (π Func π) |
3 | | eqid 2733 |
. . . . 5
β’ (π Nat π) = (π Nat π) |
4 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2733 |
. . . . 5
β’
(compβπ) =
(compβπ) |
6 | | catcfuccl.x |
. . . . . . 7
β’ (π β π β π΅) |
7 | | catcfuccl.c |
. . . . . . . 8
β’ πΆ = (CatCatβπ) |
8 | | catcfuccl.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
9 | | catcfuccl.u |
. . . . . . . 8
β’ (π β π β WUni) |
10 | 7, 8, 9 | catcbas 17992 |
. . . . . . 7
β’ (π β π΅ = (π β© Cat)) |
11 | 6, 10 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β (π β© Cat)) |
12 | 11 | elin2d 4160 |
. . . . 5
β’ (π β π β Cat) |
13 | | catcfuccl.y |
. . . . . . 7
β’ (π β π β π΅) |
14 | 13, 10 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β (π β© Cat)) |
15 | 14 | elin2d 4160 |
. . . . 5
β’ (π β π β Cat) |
16 | | eqidd 2734 |
. . . . 5
β’ (π β (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))) = (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))))) |
17 | 1, 2, 3, 4, 5, 12,
15, 16 | fucval 17851 |
. . . 4
β’ (π β π = {β¨(Baseβndx), (π Func π)β©, β¨(Hom βndx), (π Nat π)β©, β¨(compβndx), (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))))β©}) |
18 | | df-base 17089 |
. . . . . . 7
β’ Base =
Slot 1 |
19 | | catcfuccl.1 |
. . . . . . . 8
β’ (π β Ο β π) |
20 | 9, 19 | wunndx 17072 |
. . . . . . 7
β’ (π β ndx β π) |
21 | 18, 9, 20 | wunstr 17065 |
. . . . . 6
β’ (π β (Baseβndx) β
π) |
22 | 11 | elin1d 4159 |
. . . . . . 7
β’ (π β π β π) |
23 | 14 | elin1d 4159 |
. . . . . . 7
β’ (π β π β π) |
24 | 9, 22, 23 | wunfunc 17790 |
. . . . . 6
β’ (π β (π Func π) β π) |
25 | 9, 21, 24 | wunop 10663 |
. . . . 5
β’ (π β β¨(Baseβndx),
(π Func π)β© β π) |
26 | | df-hom 17162 |
. . . . . . 7
β’ Hom =
Slot ;14 |
27 | 26, 9, 20 | wunstr 17065 |
. . . . . 6
β’ (π β (Hom βndx) β
π) |
28 | 9, 22, 23 | wunnat 17848 |
. . . . . 6
β’ (π β (π Nat π) β π) |
29 | 9, 27, 28 | wunop 10663 |
. . . . 5
β’ (π β β¨(Hom βndx),
(π Nat π)β© β π) |
30 | | df-cco 17163 |
. . . . . . 7
β’ comp =
Slot ;15 |
31 | 30, 9, 20 | wunstr 17065 |
. . . . . 6
β’ (π β (compβndx) β
π) |
32 | 9, 24, 24 | wunxp 10665 |
. . . . . . . 8
β’ (π β ((π Func π) Γ (π Func π)) β π) |
33 | 9, 32, 24 | wunxp 10665 |
. . . . . . 7
β’ (π β (((π Func π) Γ (π Func π)) Γ (π Func π)) β π) |
34 | 30, 9, 23 | wunstr 17065 |
. . . . . . . . . . . . . 14
β’ (π β (compβπ) β π) |
35 | 9, 34 | wunrn 10670 |
. . . . . . . . . . . . 13
β’ (π β ran (compβπ) β π) |
36 | 9, 35 | wununi 10647 |
. . . . . . . . . . . 12
β’ (π β βͺ ran (compβπ) β π) |
37 | 9, 36 | wunrn 10670 |
. . . . . . . . . . 11
β’ (π β ran βͺ ran (compβπ) β π) |
38 | 9, 37 | wununi 10647 |
. . . . . . . . . 10
β’ (π β βͺ ran βͺ ran (compβπ) β π) |
39 | 9, 38 | wunpw 10648 |
. . . . . . . . 9
β’ (π β π« βͺ ran βͺ ran (compβπ) β π) |
40 | 18, 9, 22 | wunstr 17065 |
. . . . . . . . 9
β’ (π β (Baseβπ) β π) |
41 | 9, 39, 40 | wunmap 10667 |
. . . . . . . 8
β’ (π β (π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) β
π) |
42 | 9, 28 | wunrn 10670 |
. . . . . . . . . 10
β’ (π β ran (π Nat π) β π) |
43 | 9, 42 | wununi 10647 |
. . . . . . . . 9
β’ (π β βͺ ran (π Nat π) β π) |
44 | 9, 43, 43 | wunxp 10665 |
. . . . . . . 8
β’ (π β (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)) β π) |
45 | 9, 41, 44 | wunpm 10666 |
. . . . . . 7
β’ (π β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) β π) |
46 | | fvex 6856 |
. . . . . . . . . . 11
β’
(1st βπ£) β V |
47 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’
(2nd βπ£) β V |
48 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
β’
(π« βͺ ran βͺ
ran (compβπ)
βm (Baseβπ)) β V |
49 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π Nat π) β V |
50 | 49 | rnex 7850 |
. . . . . . . . . . . . . . . . . . 19
β’ ran
(π Nat π) β V |
51 | 50 | uniex 7679 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ ran (π Nat π) β V |
52 | 51, 51 | xpex 7688 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)) β V |
53 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) = (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) |
54 | | ovssunirn 7394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β βͺ ran
(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) |
55 | | ovssunirn 7394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β βͺ ran
(compβπ) |
56 | | rnss 5895 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β βͺ ran
(compβπ) β ran
(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β ran βͺ
ran (compβπ)) |
57 | | uniss 4874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (ran
(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β ran βͺ
ran (compβπ) β
βͺ ran (β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β βͺ ran
βͺ ran (compβπ)) |
58 | 55, 56, 57 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ ran (β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯)) β βͺ ran
βͺ ran (compβπ) |
59 | 54, 58 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β βͺ ran
βͺ ran (compβπ) |
60 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β V |
61 | 60 | elpw 4565 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran (compβπ) β ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β βͺ ran
βͺ ran (compβπ)) |
62 | 59, 61 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran (compβπ) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (Baseβπ) β ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran (compβπ)) |
64 | 53, 63 | fmpti 7061 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))):(Baseβπ)βΆπ« βͺ ran βͺ ran (compβπ) |
65 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(compβπ)
β V |
66 | 65 | rnex 7850 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ran
(compβπ) β
V |
67 | 66 | uniex 7679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ βͺ ran (compβπ) β V |
68 | 67 | rnex 7850 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ran βͺ ran (compβπ) β V |
69 | 68 | uniex 7679 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ βͺ ran βͺ ran (compβπ) β V |
70 | 69 | pwex 5336 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π«
βͺ ran βͺ ran
(compβπ) β
V |
71 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Baseβπ)
β V |
72 | 70, 71 | elmap 8812 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) β
(π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))):(Baseβπ)βΆπ« βͺ ran βͺ ran (compβπ)) |
73 | 64, 72 | mpbir 230 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) |
74 | 73 | rgen2w 3066 |
. . . . . . . . . . . . . . . . . 18
β’
βπ β
(π(π Nat π)β)βπ β (π(π Nat π)π)(π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) |
75 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) = (π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) |
76 | 75 | fmpo 8001 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(π(π Nat π)β)βπ β (π(π Nat π)π)(π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) β
(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))):((π(π Nat π)β) Γ (π(π Nat π)π))βΆ(π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))) |
77 | 74, 76 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))):((π(π Nat π)β) Γ (π(π Nat π)π))βΆ(π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) |
78 | | ovssunirn 7394 |
. . . . . . . . . . . . . . . . . 18
β’ (π(π Nat π)β) β βͺ ran
(π Nat π) |
79 | | ovssunirn 7394 |
. . . . . . . . . . . . . . . . . 18
β’ (π(π Nat π)π) β βͺ ran
(π Nat π) |
80 | | xpss12 5649 |
. . . . . . . . . . . . . . . . . 18
β’ (((π(π Nat π)β) β βͺ ran
(π Nat π) β§ (π(π Nat π)π) β βͺ ran
(π Nat π)) β ((π(π Nat π)β) Γ (π(π Nat π)π)) β (βͺ ran
(π Nat π) Γ βͺ ran
(π Nat π))) |
81 | 78, 79, 80 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’ ((π(π Nat π)β) Γ (π(π Nat π)π)) β (βͺ ran
(π Nat π) Γ βͺ ran
(π Nat π)) |
82 | | elpm2r 8786 |
. . . . . . . . . . . . . . . . 17
β’
((((π« βͺ ran βͺ ran (compβπ) βm (Baseβπ)) β V β§ (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)) β V) β§ ((π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))):((π(π Nat π)β) Γ (π(π Nat π)π))βΆ(π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ)) β§
((π(π Nat π)β) Γ (π(π Nat π)π)) β (βͺ ran
(π Nat π) Γ βͺ ran
(π Nat π)))) β (π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
83 | 48, 52, 77, 81, 82 | mp4an 692 |
. . . . . . . . . . . . . . . 16
β’ (π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) |
84 | 83 | sbcth 3755 |
. . . . . . . . . . . . . . 15
β’
((2nd βπ£) β V β [(2nd
βπ£) / π](π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
85 | | sbcel1g 4374 |
. . . . . . . . . . . . . . 15
β’
((2nd βπ£) β V β ([(2nd
βπ£) / π](π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) β β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))))) |
86 | 84, 85 | mpbid 231 |
. . . . . . . . . . . . . 14
β’
((2nd βπ£) β V β
β¦(2nd βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
87 | 47, 86 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
β¦(2nd βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) |
88 | 87 | sbcth 3755 |
. . . . . . . . . . . 12
β’
((1st βπ£) β V β [(1st
βπ£) / π]β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
89 | | sbcel1g 4374 |
. . . . . . . . . . . 12
β’
((1st βπ£) β V β ([(1st
βπ£) / π]β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) β β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))))) |
90 | 88, 89 | mpbid 231 |
. . . . . . . . . . 11
β’
((1st βπ£) β V β
β¦(1st βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
91 | 46, 90 | ax-mp 5 |
. . . . . . . . . 10
β’
β¦(1st βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) |
92 | 91 | rgen2w 3066 |
. . . . . . . . 9
β’
βπ£ β
((π Func π) Γ (π Func π))ββ β (π Func π)β¦(1st βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) |
93 | | eqid 2733 |
. . . . . . . . . 10
β’ (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))) = (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))) |
94 | 93 | fmpo 8001 |
. . . . . . . . 9
β’
(βπ£ β
((π Func π) Γ (π Func π))ββ β (π Func π)β¦(1st βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))) β ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) β (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))):(((π Func π) Γ (π Func π)) Γ (π Func π))βΆ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
95 | 92, 94 | mpbi 229 |
. . . . . . . 8
β’ (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))):(((π Func π) Γ (π Func π)) Γ (π Func π))βΆ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π))) |
96 | 95 | a1i 11 |
. . . . . . 7
β’ (π β (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))):(((π Func π) Γ (π Func π)) Γ (π Func π))βΆ((π« βͺ ran βͺ ran (compβπ) βm
(Baseβπ))
βpm (βͺ ran (π Nat π) Γ βͺ ran
(π Nat π)))) |
97 | 9, 33, 45, 96 | wunf 10668 |
. . . . . 6
β’ (π β (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯))))) β π) |
98 | 9, 31, 97 | wunop 10663 |
. . . . 5
β’ (π β β¨(compβndx),
(π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))))β© β π) |
99 | 9, 25, 29, 98 | wuntp 10652 |
. . . 4
β’ (π β {β¨(Baseβndx),
(π Func π)β©, β¨(Hom βndx), (π Nat π)β©, β¨(compβndx), (π£ β ((π Func π) Γ (π Func π)), β β (π Func π) β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (π(π Nat π)β), π β (π(π Nat π)π) β¦ (π₯ β (Baseβπ) β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β©(compβπ)((1st ββ)βπ₯))(πβπ₯)))))β©} β π) |
100 | 17, 99 | eqeltrd 2834 |
. . 3
β’ (π β π β π) |
101 | 1, 12, 15 | fuccat 17864 |
. . 3
β’ (π β π β Cat) |
102 | 100, 101 | elind 4155 |
. 2
β’ (π β π β (π β© Cat)) |
103 | 102, 10 | eleqtrrd 2837 |
1
β’ (π β π β π΅) |