Step | Hyp | Ref
| Expression |
1 | | wunfunc.1 |
. 2
β’ (π β π β WUni) |
2 | | baseid 17147 |
. . . . 5
β’ Base =
Slot (Baseβndx) |
3 | | wunfunc.3 |
. . . . 5
β’ (π β π· β π) |
4 | 2, 1, 3 | wunstr 17121 |
. . . 4
β’ (π β (Baseβπ·) β π) |
5 | | wunfunc.2 |
. . . . 5
β’ (π β πΆ β π) |
6 | 2, 1, 5 | wunstr 17121 |
. . . 4
β’ (π β (BaseβπΆ) β π) |
7 | 1, 4, 6 | wunmap 10721 |
. . 3
β’ (π β ((Baseβπ·) βm
(BaseβπΆ)) β
π) |
8 | | homid 17357 |
. . . . . . . . 9
β’ Hom =
Slot (Hom βndx) |
9 | 8, 1, 5 | wunstr 17121 |
. . . . . . . 8
β’ (π β (Hom βπΆ) β π) |
10 | 1, 9 | wunrn 10724 |
. . . . . . 7
β’ (π β ran (Hom βπΆ) β π) |
11 | 1, 10 | wununi 10701 |
. . . . . 6
β’ (π β βͺ ran (Hom βπΆ) β π) |
12 | 8, 1, 3 | wunstr 17121 |
. . . . . . . 8
β’ (π β (Hom βπ·) β π) |
13 | 1, 12 | wunrn 10724 |
. . . . . . 7
β’ (π β ran (Hom βπ·) β π) |
14 | 1, 13 | wununi 10701 |
. . . . . 6
β’ (π β βͺ ran (Hom βπ·) β π) |
15 | 1, 11, 14 | wunxp 10719 |
. . . . 5
β’ (π β (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) β
π) |
16 | 1, 15 | wunpw 10702 |
. . . 4
β’ (π β π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) β
π) |
17 | 1, 6, 6 | wunxp 10719 |
. . . 4
β’ (π β ((BaseβπΆ) Γ (BaseβπΆ)) β π) |
18 | 1, 16, 17 | wunmap 10721 |
. . 3
β’ (π β (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ))) β π) |
19 | 1, 7, 18 | wunxp 10719 |
. 2
β’ (π β (((Baseβπ·) βm
(BaseβπΆ)) Γ
(π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ)))) β π) |
20 | | relfunc 17812 |
. . . 4
β’ Rel
(πΆ Func π·) |
21 | 20 | a1i 11 |
. . 3
β’ (π β Rel (πΆ Func π·)) |
22 | | df-br 5150 |
. . . 4
β’ (π(πΆ Func π·)π β β¨π, πβ© β (πΆ Func π·)) |
23 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΆ) =
(BaseβπΆ) |
24 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ·) =
(Baseβπ·) |
25 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π(πΆ Func π·)π) β π(πΆ Func π·)π) |
26 | 23, 24, 25 | funcf1 17816 |
. . . . . . 7
β’ ((π β§ π(πΆ Func π·)π) β π:(BaseβπΆ)βΆ(Baseβπ·)) |
27 | | fvex 6905 |
. . . . . . . 8
β’
(Baseβπ·)
β V |
28 | | fvex 6905 |
. . . . . . . 8
β’
(BaseβπΆ)
β V |
29 | 27, 28 | elmap 8865 |
. . . . . . 7
β’ (π β ((Baseβπ·) βm
(BaseβπΆ)) β
π:(BaseβπΆ)βΆ(Baseβπ·)) |
30 | 26, 29 | sylibr 233 |
. . . . . 6
β’ ((π β§ π(πΆ Func π·)π) β π β ((Baseβπ·) βm (BaseβπΆ))) |
31 | | mapsspw 8872 |
. . . . . . . . . . 11
β’ (((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β π« (((Hom
βπΆ)βπ§) Γ ((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§)))) |
32 | | fvssunirn 6925 |
. . . . . . . . . . . . 13
β’ ((Hom
βπΆ)βπ§) β βͺ ran (Hom βπΆ) |
33 | | ovssunirn 7445 |
. . . . . . . . . . . . 13
β’ ((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) β βͺ ran (Hom βπ·) |
34 | | xpss12 5692 |
. . . . . . . . . . . . 13
β’ ((((Hom
βπΆ)βπ§) β βͺ ran (Hom βπΆ) β§ ((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§))) β βͺ ran (Hom βπ·)) β (((Hom βπΆ)βπ§) Γ ((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§)))) β (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))) |
35 | 32, 33, 34 | mp2an 691 |
. . . . . . . . . . . 12
β’ (((Hom
βπΆ)βπ§) Γ ((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§)))) β (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) |
36 | 35 | sspwi 4615 |
. . . . . . . . . . 11
β’ π«
(((Hom βπΆ)βπ§) Γ ((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§)))) β π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) |
37 | 31, 36 | sstri 3992 |
. . . . . . . . . 10
β’ (((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) |
38 | 37 | rgenw 3066 |
. . . . . . . . 9
β’
βπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))(((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) |
39 | | ss2ixp 8904 |
. . . . . . . . 9
β’
(βπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))(((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) β
Xπ§
β ((BaseβπΆ)
Γ (BaseβπΆ))(((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β Xπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))π«
(βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
β’ Xπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))(((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β Xπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))π«
(βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) |
41 | 28, 28 | xpex 7740 |
. . . . . . . . 9
β’
((BaseβπΆ)
Γ (BaseβπΆ))
β V |
42 | | fvex 6905 |
. . . . . . . . . . . . 13
β’ (Hom
βπΆ) β
V |
43 | 42 | rnex 7903 |
. . . . . . . . . . . 12
β’ ran (Hom
βπΆ) β
V |
44 | 43 | uniex 7731 |
. . . . . . . . . . 11
β’ βͺ ran (Hom βπΆ) β V |
45 | | fvex 6905 |
. . . . . . . . . . . . 13
β’ (Hom
βπ·) β
V |
46 | 45 | rnex 7903 |
. . . . . . . . . . . 12
β’ ran (Hom
βπ·) β
V |
47 | 46 | uniex 7731 |
. . . . . . . . . . 11
β’ βͺ ran (Hom βπ·) β V |
48 | 44, 47 | xpex 7740 |
. . . . . . . . . 10
β’ (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) β
V |
49 | 48 | pwex 5379 |
. . . . . . . . 9
β’ π«
(βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) β
V |
50 | 41, 49 | ixpconst 8901 |
. . . . . . . 8
β’ Xπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))π«
(βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·)) =
(π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ))) |
51 | 40, 50 | sseqtri 4019 |
. . . . . . 7
β’ Xπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))(((πβ(1st
βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§)) β (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ))) |
52 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπΆ) = (Hom
βπΆ) |
53 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπ·) = (Hom
βπ·) |
54 | 23, 52, 53, 25 | funcixp 17817 |
. . . . . . 7
β’ ((π β§ π(πΆ Func π·)π) β π β Xπ§ β ((BaseβπΆ) Γ (BaseβπΆ))(((πβ(1st βπ§))(Hom βπ·)(πβ(2nd βπ§))) βm ((Hom
βπΆ)βπ§))) |
55 | 51, 54 | sselid 3981 |
. . . . . 6
β’ ((π β§ π(πΆ Func π·)π) β π β (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ)))) |
56 | 30, 55 | opelxpd 5716 |
. . . . 5
β’ ((π β§ π(πΆ Func π·)π) β β¨π, πβ© β (((Baseβπ·) βm (BaseβπΆ)) Γ (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ))))) |
57 | 56 | ex 414 |
. . . 4
β’ (π β (π(πΆ Func π·)π β β¨π, πβ© β (((Baseβπ·) βm (BaseβπΆ)) Γ (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ)))))) |
58 | 22, 57 | biimtrrid 242 |
. . 3
β’ (π β (β¨π, πβ© β (πΆ Func π·) β β¨π, πβ© β (((Baseβπ·) βm (BaseβπΆ)) Γ (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ)))))) |
59 | 21, 58 | relssdv 5789 |
. 2
β’ (π β (πΆ Func π·) β (((Baseβπ·) βm (BaseβπΆ)) Γ (π« (βͺ ran (Hom βπΆ) Γ βͺ ran
(Hom βπ·))
βm ((BaseβπΆ) Γ (BaseβπΆ))))) |
60 | 1, 19, 59 | wunss 10707 |
1
β’ (π β (πΆ Func π·) β π) |