Step | Hyp | Ref
| Expression |
1 | | funcsetcestrc.s |
. . 3
β’ π = (SetCatβπ) |
2 | | funcsetcestrc.c |
. . 3
β’ πΆ = (Baseβπ) |
3 | | funcsetcestrc.f |
. . 3
β’ (π β πΉ = (π₯ β πΆ β¦ {β¨(Baseβndx), π₯β©})) |
4 | | funcsetcestrc.u |
. . 3
β’ (π β π β WUni) |
5 | | funcsetcestrc.o |
. . 3
β’ (π β Ο β π) |
6 | | funcsetcestrc.g |
. . 3
β’ (π β πΊ = (π₯ β πΆ, π¦ β πΆ β¦ ( I βΎ (π¦ βm π₯)))) |
7 | | funcsetcestrc.e |
. . 3
β’ πΈ = (ExtStrCatβπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrc 18059 |
. 2
β’ (π β πΉ(π Func πΈ)πΊ) |
9 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrclem8 18057 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ))) |
10 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β WUni) |
11 | | eqid 2737 |
. . . . . . 7
β’ (Hom
βπΈ) = (Hom
βπΈ) |
12 | 1, 2, 3, 4, 5 | funcsetcestrclem2 18050 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
13 | 12 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
14 | 1, 2, 3, 4, 5 | funcsetcestrclem2 18050 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΉβπ) β π) |
15 | 14 | adantrl 715 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (πΉβπ) β π) |
16 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
17 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(πΉβπ)) = (Baseβ(πΉβπ)) |
18 | 7, 10, 11, 13, 15, 16, 17 | elestrchom 18022 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β ((πΉβπ)(Hom βπΈ)(πΉβπ)) β β:(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)))) |
19 | 1, 2, 3 | funcsetcestrclem1 18049 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
20 | 19 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
21 | 20 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
22 | | eqid 2737 |
. . . . . . . . . . 11
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
23 | 22 | 1strbas 17107 |
. . . . . . . . . 10
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx), πβ©})) |
24 | 23 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π = (Baseβ{β¨(Baseβndx), πβ©})) |
25 | 21, 24 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
26 | 1, 2, 3 | funcsetcestrclem1 18049 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
27 | 26 | adantrl 715 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (πΉβπ) = {β¨(Baseβndx), πβ©}) |
28 | 27 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = (Baseβ{β¨(Baseβndx),
πβ©})) |
29 | | eqid 2737 |
. . . . . . . . . . 11
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
30 | 29 | 1strbas 17107 |
. . . . . . . . . 10
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx), πβ©})) |
31 | 30 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π = (Baseβ{β¨(Baseβndx), πβ©})) |
32 | 28, 31 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (Baseβ(πΉβπ)) = π) |
33 | 25, 32 | feq23d 6668 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β:(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β β:πβΆπ)) |
34 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π β πΆ β§ π β πΆ)) |
35 | 34 | ancomd 463 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π β πΆ β§ π β πΆ)) |
36 | | elmapg 8785 |
. . . . . . . . . . . . 13
β’ ((π β πΆ β§ π β πΆ) β (β β (π βm π) β β:πβΆπ)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β (π βm π) β β:πβΆπ)) |
38 | 37 | biimpar 479 |
. . . . . . . . . . 11
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β β β (π βm π)) |
39 | | equequ2 2030 |
. . . . . . . . . . . 12
β’ (π = β β (β = π β β = β)) |
40 | 39 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β§ π = β) β (β = π β β = β)) |
41 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β β = β) |
42 | 38, 40, 41 | rspcedvd 3586 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β βπ β (π βm π)β = π) |
43 | 1, 2, 3, 4, 5, 6 | funcsetcestrclem6 18055 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π β (π βm π)) β ((ππΊπ)βπ) = π) |
44 | 43 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ π β (π βm π)) β ((ππΊπ)βπ) = π) |
45 | 44 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ π β (π βm π)) β (β = ((ππΊπ)βπ) β β = π)) |
46 | 45 | rexbidva 3174 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (βπ β (π βm π)β = ((ππΊπ)βπ) β βπ β (π βm π)β = π)) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β (βπ β (π βm π)β = ((ππΊπ)βπ) β βπ β (π βm π)β = π)) |
48 | 42, 47 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β βπ β (π βm π)β = ((ππΊπ)βπ)) |
49 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (Hom
βπ) = (Hom
βπ) |
50 | 1, 4 | setcbas 17971 |
. . . . . . . . . . . . . . . . 17
β’ (π β π = (Baseβπ)) |
51 | 2, 50 | eqtr4id 2796 |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ = π) |
52 | 51 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
β’ (π β (π β πΆ β π β π)) |
53 | 52 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β (π β π β π)) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β πΆ β§ π β πΆ) β (π β π β π)) |
55 | 54 | impcom 409 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β π) |
56 | 51 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
β’ (π β (π β πΆ β π β π)) |
57 | 56 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β (π β π β π)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β πΆ β§ π β πΆ) β (π β π β π)) |
59 | 58 | impcom 409 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β π) |
60 | 1, 10, 49, 55, 59 | setchom 17973 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
61 | 60 | rexeqdv 3317 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ) β βπ β (π βm π)β = ((ππΊπ)βπ))) |
62 | 61 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β (βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ) β βπ β (π βm π)β = ((ππΊπ)βπ))) |
63 | 48, 62 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ β:πβΆπ) β βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ)) |
64 | 63 | ex 414 |
. . . . . . 7
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β:πβΆπ β βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ))) |
65 | 33, 64 | sylbid 239 |
. . . . . 6
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β:(Baseβ(πΉβπ))βΆ(Baseβ(πΉβπ)) β βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ))) |
66 | 18, 65 | sylbid 239 |
. . . . 5
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β ((πΉβπ)(Hom βπΈ)(πΉβπ)) β βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ))) |
67 | 66 | ralrimiv 3143 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ)) β ββ β ((πΉβπ)(Hom βπΈ)(πΉβπ))βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ)) |
68 | | dffo3 7057 |
. . . 4
β’ ((ππΊπ):(π(Hom βπ)π)βontoβ((πΉβπ)(Hom βπΈ)(πΉβπ)) β ((ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ)) β§ ββ β ((πΉβπ)(Hom βπΈ)(πΉβπ))βπ β (π(Hom βπ)π)β = ((ππΊπ)βπ))) |
69 | 9, 67, 68 | sylanbrc 584 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βontoβ((πΉβπ)(Hom βπΈ)(πΉβπ))) |
70 | 69 | ralrimivva 3198 |
. 2
β’ (π β βπ β πΆ βπ β πΆ (ππΊπ):(π(Hom βπ)π)βontoβ((πΉβπ)(Hom βπΈ)(πΉβπ))) |
71 | 2, 11, 49 | isfull2 17805 |
. 2
β’ (πΉ(π Full πΈ)πΊ β (πΉ(π Func πΈ)πΊ β§ βπ β πΆ βπ β πΆ (ππΊπ):(π(Hom βπ)π)βontoβ((πΉβπ)(Hom βπΈ)(πΉβπ)))) |
72 | 8, 70, 71 | sylanbrc 584 |
1
β’ (π β πΉ(π Full πΈ)πΊ) |