Step | Hyp | Ref
| Expression |
1 | | funcestrcsetc.e |
. . 3
β’ πΈ = (ExtStrCatβπ) |
2 | | funcestrcsetc.s |
. . 3
β’ π = (SetCatβπ) |
3 | | funcestrcsetc.b |
. . 3
β’ π΅ = (BaseβπΈ) |
4 | | funcestrcsetc.c |
. . 3
β’ πΆ = (Baseβπ) |
5 | | funcestrcsetc.u |
. . 3
β’ (π β π β WUni) |
6 | | funcestrcsetc.f |
. . 3
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
7 | | funcestrcsetc.g |
. . 3
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
8 | 1, 2, 3, 4, 5, 6, 7 | funcestrcsetc 18042 |
. 2
β’ (π β πΉ(πΈ Func π)πΊ) |
9 | 1, 2, 3, 4, 5, 6, 7 | funcestrcsetclem8 18040 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) |
10 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β WUni) |
11 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (Hom
βπΈ) = (Hom
βπΈ) |
12 | 1, 5 | estrcbas 18017 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π = (BaseβπΈ)) |
13 | 3, 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 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
23 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
24 | 1, 10, 11, 17, 21, 22, 23 | estrchom 18019 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Hom βπΈ)π) = ((Baseβπ) βm (Baseβπ))) |
25 | 24 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β (π(Hom βπΈ)π) β β β ((Baseβπ) βm (Baseβπ)))) |
26 | 1, 2, 3, 4, 5, 6, 7, 22, 23 | funcestrcsetclem6 18038 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅) β§ β β ((Baseβπ) βm (Baseβπ))) β ((ππΊπ)ββ) = β) |
27 | 26 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β ((Baseβπ) βm (Baseβπ)) β ((ππΊπ)ββ) = β)) |
28 | 25, 27 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β (π(Hom βπΈ)π) β ((ππΊπ)ββ) = β)) |
29 | 28 | com12 32 |
. . . . . . . . 9
β’ (β β (π(Hom βπΈ)π) β ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ)ββ) = β)) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ ((β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π)) β ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ)ββ) = β)) |
31 | 30 | impcom 409 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ (β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π))) β ((ππΊπ)ββ) = β) |
32 | 24 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β (π(Hom βπΈ)π) β π β ((Baseβπ) βm (Baseβπ)))) |
33 | 1, 2, 3, 4, 5, 6, 7, 22, 23 | funcestrcsetclem6 18038 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅) β§ π β ((Baseβπ) βm (Baseβπ))) β ((ππΊπ)βπ) = π) |
34 | 33 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β ((Baseβπ) βm (Baseβπ)) β ((ππΊπ)βπ) = π)) |
35 | 32, 34 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β (π(Hom βπΈ)π) β ((ππΊπ)βπ) = π)) |
36 | 35 | com12 32 |
. . . . . . . . 9
β’ (π β (π(Hom βπΈ)π) β ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ)βπ) = π)) |
37 | 36 | adantl 483 |
. . . . . . . 8
β’ ((β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π)) β ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ)βπ) = π)) |
38 | 37 | impcom 409 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ (β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π))) β ((ππΊπ)βπ) = π) |
39 | 31, 38 | eqeq12d 2749 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ (β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π))) β (((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
40 | 39 | biimpd 228 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ (β β (π(Hom βπΈ)π) β§ π β (π(Hom βπΈ)π))) β (((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
41 | 40 | ralrimivva 3194 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β ββ β (π(Hom βπΈ)π)βπ β (π(Hom βπΈ)π)(((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π)) |
42 | | dff13 7203 |
. . . 4
β’ ((ππΊπ):(π(Hom βπΈ)π)β1-1β((πΉβπ)(Hom βπ)(πΉβπ)) β ((ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ)) β§ ββ β (π(Hom βπΈ)π)βπ β (π(Hom βπΈ)π)(((ππΊπ)ββ) = ((ππΊπ)βπ) β β = π))) |
43 | 9, 41, 42 | sylanbrc 584 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπΈ)π)β1-1β((πΉβπ)(Hom βπ)(πΉβπ))) |
44 | 43 | ralrimivva 3194 |
. 2
β’ (π β βπ β π΅ βπ β π΅ (ππΊπ):(π(Hom βπΈ)π)β1-1β((πΉβπ)(Hom βπ)(πΉβπ))) |
45 | | eqid 2733 |
. . 3
β’ (Hom
βπ) = (Hom
βπ) |
46 | 3, 11, 45 | isfth2 17807 |
. 2
β’ (πΉ(πΈ Faith π)πΊ β (πΉ(πΈ Func π)πΊ β§ βπ β π΅ βπ β π΅ (ππΊπ):(π(Hom βπΈ)π)β1-1β((πΉβπ)(Hom βπ)(πΉβπ)))) |
47 | 8, 44, 46 | sylanbrc 584 |
1
β’ (π β πΉ(πΈ Faith π)πΊ) |