Step | Hyp | Ref
| Expression |
1 | | wunnat.1 |
. 2
β’ (π β π β WUni) |
2 | | wunnat.2 |
. . . 4
β’ (π β πΆ β π) |
3 | | wunnat.3 |
. . . 4
β’ (π β π· β π) |
4 | 1, 2, 3 | wunfunc 17846 |
. . 3
β’ (π β (πΆ Func π·) β π) |
5 | 1, 4, 4 | wunxp 10716 |
. 2
β’ (π β ((πΆ Func π·) Γ (πΆ Func π·)) β π) |
6 | | df-hom 17218 |
. . . . . . 7
β’ Hom =
Slot ;14 |
7 | 6, 1, 3 | wunstr 17118 |
. . . . . 6
β’ (π β (Hom βπ·) β π) |
8 | 1, 7 | wunrn 10721 |
. . . . 5
β’ (π β ran (Hom βπ·) β π) |
9 | 1, 8 | wununi 10698 |
. . . 4
β’ (π β βͺ ran (Hom βπ·) β π) |
10 | | df-base 17142 |
. . . . 5
β’ Base =
Slot 1 |
11 | 10, 1, 2 | wunstr 17118 |
. . . 4
β’ (π β (BaseβπΆ) β π) |
12 | 1, 9, 11 | wunmap 10718 |
. . 3
β’ (π β (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β π) |
13 | 1, 12 | wunpw 10699 |
. 2
β’ (π β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β π) |
14 | | fvex 6902 |
. . . . . 6
β’
(1st βπ) β V |
15 | | fvex 6902 |
. . . . . . . . 9
β’
(1st βπ) β V |
16 | | ovex 7439 |
. . . . . . . . . . . 12
β’ (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β V |
17 | | ssrab2 4077 |
. . . . . . . . . . . . 13
β’ {π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) |
18 | | ovssunirn 7442 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ₯)(Hom βπ·)(π βπ₯)) β βͺ ran
(Hom βπ·) |
19 | 18 | rgenw 3066 |
. . . . . . . . . . . . . . 15
β’
βπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β βͺ ran
(Hom βπ·) |
20 | | ss2ixp 8901 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β βͺ ran
(Hom βπ·) β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β Xπ₯ β (BaseβπΆ)βͺ
ran (Hom βπ·)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β Xπ₯ β (BaseβπΆ)βͺ
ran (Hom βπ·) |
22 | | fvex 6902 |
. . . . . . . . . . . . . . 15
β’
(BaseβπΆ)
β V |
23 | | fvex 6902 |
. . . . . . . . . . . . . . . . 17
β’ (Hom
βπ·) β
V |
24 | 23 | rnex 7900 |
. . . . . . . . . . . . . . . 16
β’ ran (Hom
βπ·) β
V |
25 | 24 | uniex 7728 |
. . . . . . . . . . . . . . 15
β’ βͺ ran (Hom βπ·) β V |
26 | 22, 25 | ixpconst 8898 |
. . . . . . . . . . . . . 14
β’ Xπ₯ β
(BaseβπΆ)βͺ ran (Hom βπ·) = (βͺ ran (Hom
βπ·)
βm (BaseβπΆ)) |
27 | 21, 26 | sseqtri 4018 |
. . . . . . . . . . . . 13
β’ Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β (βͺ ran
(Hom βπ·)
βm (BaseβπΆ)) |
28 | 17, 27 | sstri 3991 |
. . . . . . . . . . . 12
β’ {π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β (βͺ ran
(Hom βπ·)
βm (BaseβπΆ)) |
29 | 16, 28 | elpwi2 5346 |
. . . . . . . . . . 11
β’ {π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) |
30 | 29 | sbcth 3792 |
. . . . . . . . . 10
β’
((1st βπ) β V β [(1st
βπ) / π ]{π β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
31 | | sbcel1g 4413 |
. . . . . . . . . 10
β’
((1st βπ) β V β ([(1st
βπ) / π ]{π β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β
β¦(1st βπ) / π β¦{π β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)))) |
32 | 30, 31 | mpbid 231 |
. . . . . . . . 9
β’
((1st βπ) β V β
β¦(1st βπ) / π β¦{π β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
33 | 15, 32 | ax-mp 5 |
. . . . . . . 8
β’
β¦(1st βπ) / π β¦{π β Xπ₯ β (BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) |
34 | 33 | sbcth 3792 |
. . . . . . 7
β’
((1st βπ) β V β [(1st
βπ) / π]β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
35 | | sbcel1g 4413 |
. . . . . . 7
β’
((1st βπ) β V β ([(1st
βπ) / π]β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β
β¦(1st βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)))) |
36 | 34, 35 | mpbid 231 |
. . . . . 6
β’
((1st βπ) β V β
β¦(1st βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
37 | 14, 36 | ax-mp 5 |
. . . . 5
β’
β¦(1st βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) |
38 | 37 | rgen2w 3067 |
. . . 4
β’
βπ β
(πΆ Func π·)βπ β (πΆ Func π·)β¦(1st βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) |
39 | | eqid 2733 |
. . . . . 6
β’ (πΆ Nat π·) = (πΆ Nat π·) |
40 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
41 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
42 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ·) = (Hom
βπ·) |
43 | | eqid 2733 |
. . . . . 6
β’
(compβπ·) =
(compβπ·) |
44 | 39, 40, 41, 42, 43 | natfval 17894 |
. . . . 5
β’ (πΆ Nat π·) = (π β (πΆ Func π·), π β (πΆ Func π·) β¦ β¦(1st
βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))}) |
45 | 44 | fmpo 8051 |
. . . 4
β’
(βπ β
(πΆ Func π·)βπ β (πΆ Func π·)β¦(1st βπ) / πβ¦β¦(1st
βπ) / π β¦{π β Xπ₯ β
(BaseβπΆ)((πβπ₯)(Hom βπ·)(π βπ₯)) β£ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)βπ§ β (π₯(Hom βπΆ)π¦)((πβπ¦)(β¨(πβπ₯), (πβπ¦)β©(compβπ·)(π βπ¦))((π₯(2nd βπ)π¦)βπ§)) = (((π₯(2nd βπ)π¦)βπ§)(β¨(πβπ₯), (π βπ₯)β©(compβπ·)(π βπ¦))(πβπ₯))} β π« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) β (πΆ Nat π·):((πΆ Func π·) Γ (πΆ Func π·))βΆπ« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
46 | 38, 45 | mpbi 229 |
. . 3
β’ (πΆ Nat π·):((πΆ Func π·) Γ (πΆ Func π·))βΆπ« (βͺ ran (Hom βπ·) βm (BaseβπΆ)) |
47 | 46 | a1i 11 |
. 2
β’ (π β (πΆ Nat π·):((πΆ Func π·) Γ (πΆ Func π·))βΆπ« (βͺ ran (Hom βπ·) βm (BaseβπΆ))) |
48 | 1, 5, 13, 47 | wunf 10719 |
1
β’ (π β (πΆ Nat π·) β π) |