Step | Hyp | Ref
| Expression |
1 | | f1oi 6823 |
. . . 4
β’ ( I
βΎ ((Baseβπ)
βm (Baseβπ))):((Baseβπ) βm (Baseβπ))β1-1-ontoβ((Baseβπ) βm (Baseβπ)) |
2 | | f1of 6785 |
. . . 4
β’ (( I
βΎ ((Baseβπ)
βm (Baseβπ))):((Baseβπ) βm (Baseβπ))β1-1-ontoβ((Baseβπ) βm (Baseβπ)) β ( I βΎ
((Baseβπ)
βm (Baseβπ))):((Baseβπ) βm (Baseβπ))βΆ((Baseβπ) βm
(Baseβπ))) |
3 | 1, 2 | mp1i 13 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ ((Baseβπ) βm
(Baseβπ))):((Baseβπ) βm (Baseβπ))βΆ((Baseβπ) βm
(Baseβπ))) |
4 | | elmapi 8790 |
. . . . 5
β’ (π β ((Baseβπ) βm
(Baseβπ)) β
π:(Baseβπ)βΆ(Baseβπ)) |
5 | | fvex 6856 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
6 | | fvex 6856 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
7 | 5, 6 | pm3.2i 472 |
. . . . . . . . 9
β’
((Baseβπ)
β V β§ (Baseβπ) β V) |
8 | | elmapg 8781 |
. . . . . . . . . 10
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (π β ((Baseβπ) βm (Baseβπ)) β π:(Baseβπ)βΆ(Baseβπ))) |
9 | 8 | bicomd 222 |
. . . . . . . . 9
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((Baseβπ) βm (Baseβπ)))) |
10 | 7, 9 | mp1i 13 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((Baseβπ) βm (Baseβπ)))) |
11 | 10 | biimpa 478 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β π β ((Baseβπ) βm (Baseβπ))) |
12 | | funcestrcsetc.e |
. . . . . . . . . . 11
β’ πΈ = (ExtStrCatβπ) |
13 | | funcestrcsetc.s |
. . . . . . . . . . 11
β’ π = (SetCatβπ) |
14 | | funcestrcsetc.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΈ) |
15 | | funcestrcsetc.c |
. . . . . . . . . . 11
β’ πΆ = (Baseβπ) |
16 | | funcestrcsetc.u |
. . . . . . . . . . 11
β’ (π β π β WUni) |
17 | | funcestrcsetc.f |
. . . . . . . . . . 11
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
18 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem1 18033 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
19 | 18 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
20 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem1 18033 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
21 | 20 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) = (Baseβπ)) |
22 | 19, 21 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((πΉβπ) βm (πΉβπ)) = ((Baseβπ) βm (Baseβπ))) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β ((πΉβπ) βm (πΉβπ)) = ((Baseβπ) βm (Baseβπ))) |
24 | 11, 23 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π:(Baseβπ)βΆ(Baseβπ)) β π β ((πΉβπ) βm (πΉβπ))) |
25 | 24 | ex 414 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π:(Baseβπ)βΆ(Baseβπ) β π β ((πΉβπ) βm (πΉβπ)))) |
26 | 4, 25 | syl5 34 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β ((Baseβπ) βm (Baseβπ)) β π β ((πΉβπ) βm (πΉβπ)))) |
27 | 26 | ssrdv 3951 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((Baseβπ) βm (Baseβπ)) β ((πΉβπ) βm (πΉβπ))) |
28 | 3, 27 | fssd 6687 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ ((Baseβπ) βm
(Baseβπ))):((Baseβπ) βm (Baseβπ))βΆ((πΉβπ) βm (πΉβπ))) |
29 | | funcestrcsetc.g |
. . . 4
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
30 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
31 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
32 | 12, 13, 14, 15, 16, 17, 29, 30, 31 | funcestrcsetclem5 18037 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ ((Baseβπ) βm
(Baseβπ)))) |
33 | 16 | adantr 482 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β WUni) |
34 | | eqid 2733 |
. . . 4
β’ (Hom
βπΈ) = (Hom
βπΈ) |
35 | 12, 16 | estrcbas 18017 |
. . . . . . . . 9
β’ (π β π = (BaseβπΈ)) |
36 | 14, 35 | eqtr4id 2792 |
. . . . . . . 8
β’ (π β π΅ = π) |
37 | 36 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π β π΅ β π β π)) |
38 | 37 | biimpcd 249 |
. . . . . 6
β’ (π β π΅ β (π β π β π)) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β (π β π β π)) |
40 | 39 | impcom 409 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
41 | 36 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π β π΅ β π β π)) |
42 | 41 | biimpd 228 |
. . . . . 6
β’ (π β (π β π΅ β π β π)) |
43 | 42 | adantld 492 |
. . . . 5
β’ (π β ((π β π΅ β§ π β π΅) β π β π)) |
44 | 43 | imp 408 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
45 | 12, 33, 34, 40, 44, 30, 31 | estrchom 18019 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Hom βπΈ)π) = ((Baseβπ) βm (Baseβπ))) |
46 | | eqid 2733 |
. . . 4
β’ (Hom
βπ) = (Hom
βπ) |
47 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem2 18034 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
48 | 47 | adantrr 716 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
49 | 12, 13, 14, 15, 16, 17 | funcestrcsetclem2 18034 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβπ) β π) |
50 | 49 | adantrl 715 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΉβπ) β π) |
51 | 13, 33, 46, 48, 50 | setchom 17971 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((πΉβπ)(Hom βπ)(πΉβπ)) = ((πΉβπ) βm (πΉβπ))) |
52 | 32, 45, 51 | feq123d 6658 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ)) β ( I βΎ ((Baseβπ) βm
(Baseβπ))):((Baseβπ) βm (Baseβπ))βΆ((πΉβπ) βm (πΉβπ)))) |
53 | 28, 52 | mpbird 257 |
1
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπΈ)π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) |