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 18057 |
. 2
β’ (π β πΉ(π Func πΈ)πΊ) |
9 | 1, 2, 3, 4, 5, 6, 7 | funcsetcestrclem8 18055 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ))) |
10 | 4 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β WUni) |
11 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (Hom
βπ) = (Hom
βπ) |
12 | 1, 4 | setcbas 17969 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π = (Baseβπ)) |
13 | 2, 12 | eqtr4id 2792 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΆ = π) |
14 | 13 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β πΆ β π β π)) |
15 | 14 | biimpcd 249 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β (π β π β π)) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β πΆ β§ π β πΆ) β (π β π β π)) |
17 | 16 | impcom 409 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β π) |
18 | 13 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β πΆ β π β π)) |
19 | 18 | biimpcd 249 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β (π β π β π)) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β πΆ β§ π β πΆ) β (π β π β π)) |
21 | 20 | impcom 409 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β πΆ)) β π β π) |
22 | 1, 10, 11, 17, 21 | setchom 17971 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π(Hom βπ)π) = (π βm π)) |
23 | 22 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β (π(Hom βπ)π) β β β (π βm π))) |
24 | 1, 2, 3, 4, 5, 6 | funcsetcestrclem6 18053 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ β β (π βm π)) β ((ππΊπ)ββ) = β) |
25 | 24 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β (π βm π) β ((ππΊπ)ββ) = β)) |
26 | 23, 25 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (β β (π(Hom βπ)π) β ((ππΊπ)ββ) = β)) |
27 | 26 | com12 32 |
. . . . . . . . 9
β’ (β β (π(Hom βπ)π) β ((π β§ (π β πΆ β§ π β πΆ)) β ((ππΊπ)ββ) = β)) |
28 | 27 | adantr 482 |
. . . . . . . 8
β’ ((β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π)) β ((π β§ (π β πΆ β§ π β πΆ)) β ((ππΊπ)ββ) = β)) |
29 | 28 | impcom 409 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ (β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π))) β ((ππΊπ)ββ) = β) |
30 | 22 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π β (π(Hom βπ)π) β π β (π βm π))) |
31 | 1, 2, 3, 4, 5, 6 | funcsetcestrclem6 18053 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β πΆ) β§ π β (π βm π)) β ((ππΊπ)βπ) = π) |
32 | 31 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π β (π βm π) β ((ππΊπ)βπ) = π)) |
33 | 30, 32 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (π β (π(Hom βπ)π) β ((ππΊπ)βπ) = π)) |
34 | 33 | com12 32 |
. . . . . . . . 9
β’ (π β (π(Hom βπ)π) β ((π β§ (π β πΆ β§ π β πΆ)) β ((ππΊπ)βπ) = π)) |
35 | 34 | adantl 483 |
. . . . . . . 8
β’ ((β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π)) β ((π β§ (π β πΆ β§ π β πΆ)) β ((ππΊπ)βπ) = π)) |
36 | 35 | impcom 409 |
. . . . . . 7
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ (β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π))) β ((ππΊπ)βπ) = π) |
37 | 29, 36 | eqeq12d 2749 |
. . . . . 6
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ (β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π))) β (((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
38 | 37 | biimpd 228 |
. . . . 5
β’ (((π β§ (π β πΆ β§ π β πΆ)) β§ (β β (π(Hom βπ)π) β§ π β (π(Hom βπ)π))) β (((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
39 | 38 | ralrimivva 3194 |
. . . 4
β’ ((π β§ (π β πΆ β§ π β πΆ)) β ββ β (π(Hom βπ)π)βπ β (π(Hom βπ)π)(((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
40 | | dff13 7203 |
. . . 4
β’ ((ππΊπ):(π(Hom βπ)π)β1-1β((πΉβπ)(Hom βπΈ)(πΉβπ)) β ((ππΊπ):(π(Hom βπ)π)βΆ((πΉβπ)(Hom βπΈ)(πΉβπ)) β§ ββ β (π(Hom βπ)π)βπ β (π(Hom βπ)π)(((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π))) |
41 | 9, 39, 40 | sylanbrc 584 |
. . 3
β’ ((π β§ (π β πΆ β§ π β πΆ)) β (ππΊπ):(π(Hom βπ)π)β1-1β((πΉβπ)(Hom βπΈ)(πΉβπ))) |
42 | 41 | ralrimivva 3194 |
. 2
β’ (π β βπ β πΆ βπ β πΆ (ππΊπ):(π(Hom βπ)π)β1-1β((πΉβπ)(Hom βπΈ)(πΉβπ))) |
43 | | eqid 2733 |
. . 3
β’ (Hom
βπΈ) = (Hom
βπΈ) |
44 | 2, 11, 43 | isfth2 17807 |
. 2
β’ (πΉ(π Faith πΈ)πΊ β (πΉ(π Func πΈ)πΊ β§ βπ β πΆ βπ β πΆ (ππΊπ):(π(Hom βπ)π)β1-1β((πΉβπ)(Hom βπΈ)(πΉβπ)))) |
45 | 8, 42, 44 | sylanbrc 584 |
1
β’ (π β πΉ(π Faith πΈ)πΊ) |