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 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β WUni) |
11 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπ) = (Hom
βπ) |
12 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem2 18034 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
13 | 12 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
14 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem2 18034 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
15 | 14 | adantrl 715 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
16 | 2, 10, 11, 13, 15 | elsetchom 17972 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β ((πΉβπ)(Hom βπ)(πΉβπ)) β β:(πΉβπ)βΆ(πΉβπ))) |
17 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18033 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
18 | 17 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
19 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18033 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
20 | 19 | adantrl 715 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
21 | 18, 20 | feq23d 6664 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β:(πΉβπ)βΆ(πΉβπ) β β:(Baseβπ)βΆ(Baseβπ))) |
22 | 16, 21 | bitrd 279 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β ((πΉβπ)(Hom βπ)(πΉβπ)) β β:(Baseβπ)βΆ(Baseβπ))) |
23 | | fvex 6856 |
. . . . . . . . . . . . 13
β’
(Baseβπ)
β V |
24 | | fvex 6856 |
. . . . . . . . . . . . 13
β’
(Baseβπ)
β V |
25 | 23, 24 | pm3.2i 472 |
. . . . . . . . . . . 12
β’
((Baseβπ)
β V β§ (Baseβπ) β V) |
26 | | elmapg 8781 |
. . . . . . . . . . . 12
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (β β ((Baseβπ) βm (Baseβπ)) β β:(Baseβπ)βΆ(Baseβπ))) |
27 | 25, 26 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β ((Baseβπ) βm (Baseβπ)) β β:(Baseβπ)βΆ(Baseβπ))) |
28 | 27 | biimpar 479 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β β β ((Baseβπ) βm (Baseβπ))) |
29 | | equequ2 2030 |
. . . . . . . . . . 11
β’ (π = β β (β = π β β = β)) |
30 | 29 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β§ π = β) β (β = π β β = β)) |
31 | | eqidd 2734 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β β = β) |
32 | 28, 30, 31 | rspcedvd 3582 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β βπ β ((Baseβπ) βm (Baseβπ))β = π) |
33 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
34 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
35 | 1, 2, 3, 4, 5, 6, 7, 33, 34 | funcestrcsetclem6 18038 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅) β§ π β ((Baseβπ) βm (Baseβπ))) β ((ππΊπ)βπ) = π) |
36 | 35 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β ((Baseβπ) βm (Baseβπ))) β ((ππΊπ)βπ) = π) |
37 | 36 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β ((Baseβπ) βm (Baseβπ))) β (β = ((ππΊπ)βπ) β β = π)) |
38 | 37 | rexbidva 3170 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ β ((Baseβπ) βm (Baseβπ))β = ((ππΊπ)βπ) β βπ β ((Baseβπ) βm (Baseβπ))β = π)) |
39 | 38 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β (βπ β ((Baseβπ) βm (Baseβπ))β = ((ππΊπ)βπ) β βπ β ((Baseβπ) βm (Baseβπ))β = π)) |
40 | 32, 39 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β βπ β ((Baseβπ) βm (Baseβπ))β = ((ππΊπ)βπ)) |
41 | | eqid 2733 |
. . . . . . . . . . 11
β’ (Hom
βπΈ) = (Hom
βπΈ) |
42 | 1, 5 | estrcbas 18017 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (BaseβπΈ)) |
43 | 3, 42 | eqtr4id 2792 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ = π) |
44 | 43 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π β π΅ β π β π)) |
45 | 44 | biimpcd 249 |
. . . . . . . . . . . . 13
β’ (π β π΅ β (π β π β π)) |
46 | 45 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π β π΅) β (π β π β π)) |
47 | 46 | impcom 409 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
48 | 43 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π β π΅ β π β π)) |
49 | 48 | biimpcd 249 |
. . . . . . . . . . . . 13
β’ (π β π΅ β (π β π β π)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π β π΅) β (π β π β π)) |
51 | 50 | impcom 409 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
52 | 1, 10, 41, 47, 51, 33, 34 | estrchom 18019 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Hom βπΈ)π) = ((Baseβπ) βm (Baseβπ))) |
53 | 52 | rexeqdv 3313 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ) β βπ β ((Baseβπ) βm (Baseβπ))β = ((ππΊπ)βπ))) |
54 | 53 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β (βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ) β βπ β ((Baseβπ) βm (Baseβπ))β = ((ππΊπ)βπ))) |
55 | 40, 54 | mpbird 257 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ β:(Baseβπ)βΆ(Baseβπ)) β βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ)) |
56 | 55 | ex 414 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β:(Baseβπ)βΆ(Baseβπ) β βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ))) |
57 | 22, 56 | sylbid 239 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (β β ((πΉβπ)(Hom βπ)(πΉβπ)) β βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ))) |
58 | 57 | ralrimiv 3139 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β ββ β ((πΉβπ)(Hom βπ)(πΉβπ))βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ)) |
59 | | dffo3 7053 |
. . . 4
β’ ((ππΊπ):(π(Hom βπΈ)π)βontoβ((πΉβπ)(Hom βπ)(πΉβπ)) β ((ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ)) β§ ββ β ((πΉβπ)(Hom βπ)(πΉβπ))βπ β (π(Hom βπΈ)π)β = ((ππΊπ)βπ))) |
60 | 9, 58, 59 | sylanbrc 584 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπΈ)π)βontoβ((πΉβπ)(Hom βπ)(πΉβπ))) |
61 | 60 | ralrimivva 3194 |
. 2
β’ (π β βπ β π΅ βπ β π΅ (ππΊπ):(π(Hom βπΈ)π)βontoβ((πΉβπ)(Hom βπ)(πΉβπ))) |
62 | 3, 11, 41 | isfull2 17803 |
. 2
β’ (πΉ(πΈ Full π)πΊ β (πΉ(πΈ Func π)πΊ β§ βπ β π΅ βπ β π΅ (ππΊπ):(π(Hom βπΈ)π)βontoβ((πΉβπ)(Hom βπ)(πΉβπ)))) |
63 | 8, 61, 62 | sylanbrc 584 |
1
β’ (π β πΉ(πΈ Full π)πΊ) |