Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
2 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2733 |
. . . . . 6
β’
(compβπΆ) =
(compβπΆ) |
4 | | setcepi.h |
. . . . . 6
β’ πΈ = (EpiβπΆ) |
5 | | setcmon.u |
. . . . . . 7
β’ (π β π β π) |
6 | | setcmon.c |
. . . . . . . 8
β’ πΆ = (SetCatβπ) |
7 | 6 | setccat 17976 |
. . . . . . 7
β’ (π β π β πΆ β Cat) |
8 | 5, 7 | syl 17 |
. . . . . 6
β’ (π β πΆ β Cat) |
9 | | setcmon.x |
. . . . . . 7
β’ (π β π β π) |
10 | 6, 5 | setcbas 17969 |
. . . . . . 7
β’ (π β π = (BaseβπΆ)) |
11 | 9, 10 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β (BaseβπΆ)) |
12 | | setcmon.y |
. . . . . . 7
β’ (π β π β π) |
13 | 12, 10 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β (BaseβπΆ)) |
14 | 1, 2, 3, 4, 8, 11,
13 | epihom 17630 |
. . . . 5
β’ (π β (ππΈπ) β (π(Hom βπΆ)π)) |
15 | 14 | sselda 3945 |
. . . 4
β’ ((π β§ πΉ β (ππΈπ)) β πΉ β (π(Hom βπΆ)π)) |
16 | 6, 5, 2, 9, 12 | elsetchom 17972 |
. . . . 5
β’ (π β (πΉ β (π(Hom βπΆ)π) β πΉ:πβΆπ)) |
17 | 16 | biimpa 478 |
. . . 4
β’ ((π β§ πΉ β (π(Hom βπΆ)π)) β πΉ:πβΆπ) |
18 | 15, 17 | syldan 592 |
. . 3
β’ ((π β§ πΉ β (ππΈπ)) β πΉ:πβΆπ) |
19 | 18 | frnd 6677 |
. . . 4
β’ ((π β§ πΉ β (ππΈπ)) β ran πΉ β π) |
20 | 18 | ffnd 6670 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ β (ππΈπ)) β πΉ Fn π) |
21 | | fnfvelrn 7032 |
. . . . . . . . . . . . . 14
β’ ((πΉ Fn π β§ π₯ β π) β (πΉβπ₯) β ran πΉ) |
22 | 20, 21 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ β (ππΈπ)) β§ π₯ β π) β (πΉβπ₯) β ran πΉ) |
23 | 22 | iftrued 4495 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΈπ)) β§ π₯ β π) β if((πΉβπ₯) β ran πΉ, 1o, β
) =
1o) |
24 | 23 | mpteq2dva 5206 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β (π₯ β π β¦ if((πΉβπ₯) β ran πΉ, 1o, β
)) = (π₯ β π β¦ 1o)) |
25 | 18 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ β (ππΈπ)) β§ π₯ β π) β (πΉβπ₯) β π) |
26 | 18 | feqmptd 6911 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΈπ)) β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
27 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΈπ)) β (π β π β¦ if(π β ran πΉ, 1o, β
)) = (π β π β¦ if(π β ran πΉ, 1o, β
))) |
28 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π = (πΉβπ₯) β (π β ran πΉ β (πΉβπ₯) β ran πΉ)) |
29 | 28 | ifbid 4510 |
. . . . . . . . . . . 12
β’ (π = (πΉβπ₯) β if(π β ran πΉ, 1o, β
) = if((πΉβπ₯) β ran πΉ, 1o, β
)) |
30 | 25, 26, 27, 29 | fmptco 7076 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β ((π β π β¦ if(π β ran πΉ, 1o, β
)) β πΉ) = (π₯ β π β¦ if((πΉβπ₯) β ran πΉ, 1o, β
))) |
31 | | fconstmpt 5695 |
. . . . . . . . . . . . 13
β’ (π Γ {1o}) =
(π β π β¦ 1o) |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ β (ππΈπ)) β (π Γ {1o}) = (π β π β¦ 1o)) |
33 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (π = (πΉβπ₯) β 1o =
1o) |
34 | 25, 26, 32, 33 | fmptco 7076 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β ((π Γ {1o}) β πΉ) = (π₯ β π β¦ 1o)) |
35 | 24, 30, 34 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β ((π β π β¦ if(π β ran πΉ, 1o, β
)) β πΉ) = ((π Γ {1o}) β πΉ)) |
36 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β π β π) |
37 | 9 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β π β π) |
38 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β π β π) |
39 | | setcepi.2 |
. . . . . . . . . . . 12
β’ (π β 2o β π) |
40 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β 2o β π) |
41 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β π β¦ if(π β ran πΉ, 1o, β
)) = (π β π β¦ if(π β ran πΉ, 1o, β
)) |
42 | | 1oex 8423 |
. . . . . . . . . . . . . . . . 17
β’
1o β V |
43 | 42 | prid2 4725 |
. . . . . . . . . . . . . . . 16
β’
1o β {β
, 1o} |
44 | | df2o3 8421 |
. . . . . . . . . . . . . . . 16
β’
2o = {β
, 1o} |
45 | 43, 44 | eleqtrri 2833 |
. . . . . . . . . . . . . . 15
β’
1o β 2o |
46 | | 0ex 5265 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
47 | 46 | prid1 4724 |
. . . . . . . . . . . . . . . 16
β’ β
β {β
, 1o} |
48 | 47, 44 | eleqtrri 2833 |
. . . . . . . . . . . . . . 15
β’ β
β 2o |
49 | 45, 48 | ifcli 4534 |
. . . . . . . . . . . . . 14
β’ if(π β ran πΉ, 1o, β
) β
2o |
50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π β if(π β ran πΉ, 1o, β
) β
2o) |
51 | 41, 50 | fmpti 7061 |
. . . . . . . . . . . 12
β’ (π β π β¦ if(π β ran πΉ, 1o, β
)):πβΆ2o |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β (π β π β¦ if(π β ran πΉ, 1o, β
)):πβΆ2o) |
53 | 6, 36, 3, 37, 38, 40, 18, 52 | setcco 17974 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β ((π β π β¦ if(π β ran πΉ, 1o, β
))(β¨π, πβ©(compβπΆ)2o)πΉ) = ((π β π β¦ if(π β ran πΉ, 1o, β
)) β πΉ)) |
54 | | fconst6g 6732 |
. . . . . . . . . . . 12
β’
(1o β 2o β (π Γ {1o}):πβΆ2o) |
55 | 45, 54 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β (π Γ {1o}):πβΆ2o) |
56 | 6, 36, 3, 37, 38, 40, 18, 55 | setcco 17974 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β ((π Γ {1o})(β¨π, πβ©(compβπΆ)2o)πΉ) = ((π Γ {1o}) β πΉ)) |
57 | 35, 53, 56 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((π β§ πΉ β (ππΈπ)) β ((π β π β¦ if(π β ran πΉ, 1o, β
))(β¨π, πβ©(compβπΆ)2o)πΉ) = ((π Γ {1o})(β¨π, πβ©(compβπΆ)2o)πΉ)) |
58 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β πΆ β Cat) |
59 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β π β (BaseβπΆ)) |
60 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β π β (BaseβπΆ)) |
61 | 39, 10 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ (π β 2o β
(BaseβπΆ)) |
62 | 61 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β 2o β
(BaseβπΆ)) |
63 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β πΉ β (ππΈπ)) |
64 | 6, 36, 2, 38, 40 | elsetchom 17972 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β ((π β π β¦ if(π β ran πΉ, 1o, β
)) β (π(Hom βπΆ)2o) β (π β π β¦ if(π β ran πΉ, 1o, β
)):πβΆ2o)) |
65 | 52, 64 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β (π β π β¦ if(π β ran πΉ, 1o, β
)) β (π(Hom βπΆ)2o)) |
66 | 6, 36, 2, 38, 40 | elsetchom 17972 |
. . . . . . . . . . 11
β’ ((π β§ πΉ β (ππΈπ)) β ((π Γ {1o}) β (π(Hom βπΆ)2o) β (π Γ {1o}):πβΆ2o)) |
67 | 55, 66 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (ππΈπ)) β (π Γ {1o}) β (π(Hom βπΆ)2o)) |
68 | 1, 2, 3, 4, 58, 59, 60, 62, 63, 65, 67 | epii 17631 |
. . . . . . . . 9
β’ ((π β§ πΉ β (ππΈπ)) β (((π β π β¦ if(π β ran πΉ, 1o, β
))(β¨π, πβ©(compβπΆ)2o)πΉ) = ((π Γ {1o})(β¨π, πβ©(compβπΆ)2o)πΉ) β (π β π β¦ if(π β ran πΉ, 1o, β
)) = (π Γ
{1o}))) |
69 | 57, 68 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ πΉ β (ππΈπ)) β (π β π β¦ if(π β ran πΉ, 1o, β
)) = (π Γ
{1o})) |
70 | 69, 31 | eqtrdi 2789 |
. . . . . . 7
β’ ((π β§ πΉ β (ππΈπ)) β (π β π β¦ if(π β ran πΉ, 1o, β
)) = (π β π β¦ 1o)) |
71 | 49 | rgenw 3065 |
. . . . . . . 8
β’
βπ β
π if(π β ran πΉ, 1o, β
) β
2o |
72 | | mpteqb 6968 |
. . . . . . . 8
β’
(βπ β
π if(π β ran πΉ, 1o, β
) β
2o β ((π
β π β¦ if(π β ran πΉ, 1o, β
)) = (π β π β¦ 1o) β βπ β π if(π β ran πΉ, 1o, β
) =
1o)) |
73 | 71, 72 | ax-mp 5 |
. . . . . . 7
β’ ((π β π β¦ if(π β ran πΉ, 1o, β
)) = (π β π β¦ 1o) β βπ β π if(π β ran πΉ, 1o, β
) =
1o) |
74 | 70, 73 | sylib 217 |
. . . . . 6
β’ ((π β§ πΉ β (ππΈπ)) β βπ β π if(π β ran πΉ, 1o, β
) =
1o) |
75 | | 1n0 8435 |
. . . . . . . . . 10
β’
1o β β
|
76 | 75 | nesymi 2998 |
. . . . . . . . 9
β’ Β¬
β
= 1o |
77 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π β ran πΉ β if(π β ran πΉ, 1o, β
) =
β
) |
78 | 77 | eqeq1d 2735 |
. . . . . . . . 9
β’ (Β¬
π β ran πΉ β (if(π β ran πΉ, 1o, β
) = 1o
β β
= 1o)) |
79 | 76, 78 | mtbiri 327 |
. . . . . . . 8
β’ (Β¬
π β ran πΉ β Β¬ if(π β ran πΉ, 1o, β
) =
1o) |
80 | 79 | con4i 114 |
. . . . . . 7
β’ (if(π β ran πΉ, 1o, β
) = 1o
β π β ran πΉ) |
81 | 80 | ralimi 3083 |
. . . . . 6
β’
(βπ β
π if(π β ran πΉ, 1o, β
) = 1o
β βπ β
π π β ran πΉ) |
82 | 74, 81 | syl 17 |
. . . . 5
β’ ((π β§ πΉ β (ππΈπ)) β βπ β π π β ran πΉ) |
83 | | dfss3 3933 |
. . . . 5
β’ (π β ran πΉ β βπ β π π β ran πΉ) |
84 | 82, 83 | sylibr 233 |
. . . 4
β’ ((π β§ πΉ β (ππΈπ)) β π β ran πΉ) |
85 | 19, 84 | eqssd 3962 |
. . 3
β’ ((π β§ πΉ β (ππΈπ)) β ran πΉ = π) |
86 | | dffo2 6761 |
. . 3
β’ (πΉ:πβontoβπ β (πΉ:πβΆπ β§ ran πΉ = π)) |
87 | 18, 85, 86 | sylanbrc 584 |
. 2
β’ ((π β§ πΉ β (ππΈπ)) β πΉ:πβontoβπ) |
88 | | fof 6757 |
. . . . 5
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
89 | 88 | adantl 483 |
. . . 4
β’ ((π β§ πΉ:πβontoβπ) β πΉ:πβΆπ) |
90 | 16 | biimpar 479 |
. . . 4
β’ ((π β§ πΉ:πβΆπ) β πΉ β (π(Hom βπΆ)π)) |
91 | 89, 90 | syldan 592 |
. . 3
β’ ((π β§ πΉ:πβontoβπ) β πΉ β (π(Hom βπΆ)π)) |
92 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ:πβontoβπ) β π = (BaseβπΆ)) |
93 | 92 | eleq2d 2820 |
. . . . 5
β’ ((π β§ πΉ:πβontoβπ) β (π§ β π β π§ β (BaseβπΆ))) |
94 | 5 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π β π) |
95 | 9 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π β π) |
96 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π β π) |
97 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π§ β π) |
98 | 89 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β πΉ:πβΆπ) |
99 | | simprrl 780 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π β (π(Hom βπΆ)π§)) |
100 | 6, 94, 2, 96, 97 | elsetchom 17972 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β (π β (π(Hom βπΆ)π§) β π:πβΆπ§)) |
101 | 99, 100 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π:πβΆπ§) |
102 | 6, 94, 3, 95, 96, 97, 98, 101 | setcco 17974 |
. . . . . . . . . 10
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β (π(β¨π, πβ©(compβπΆ)π§)πΉ) = (π β πΉ)) |
103 | | simprrr 781 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β β β (π(Hom βπΆ)π§)) |
104 | 6, 94, 2, 96, 97 | elsetchom 17972 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β (β β (π(Hom βπΆ)π§) β β:πβΆπ§)) |
105 | 103, 104 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β β:πβΆπ§) |
106 | 6, 94, 3, 95, 96, 97, 98, 105 | setcco 17974 |
. . . . . . . . . 10
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β (β(β¨π, πβ©(compβπΆ)π§)πΉ) = (β β πΉ)) |
107 | 102, 106 | eqeq12d 2749 |
. . . . . . . . 9
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β ((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β (π β πΉ) = (β β πΉ))) |
108 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β πΉ:πβontoβπ) |
109 | 101 | ffnd 6670 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β π Fn π) |
110 | 105 | ffnd 6670 |
. . . . . . . . . . 11
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β β Fn π) |
111 | | cocan2 7239 |
. . . . . . . . . . 11
β’ ((πΉ:πβontoβπ β§ π Fn π β§ β Fn π) β ((π β πΉ) = (β β πΉ) β π = β)) |
112 | 108, 109,
110, 111 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β ((π β πΉ) = (β β πΉ) β π = β)) |
113 | 112 | biimpd 228 |
. . . . . . . . 9
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β ((π β πΉ) = (β β πΉ) β π = β)) |
114 | 107, 113 | sylbid 239 |
. . . . . . . 8
β’ (((π β§ πΉ:πβontoβπ) β§ (π§ β π β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§)))) β ((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)) |
115 | 114 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ πΉ:πβontoβπ) β§ π§ β π) β§ (π β (π(Hom βπΆ)π§) β§ β β (π(Hom βπΆ)π§))) β ((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)) |
116 | 115 | ralrimivva 3194 |
. . . . . 6
β’ (((π β§ πΉ:πβontoβπ) β§ π§ β π) β βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)) |
117 | 116 | ex 414 |
. . . . 5
β’ ((π β§ πΉ:πβontoβπ) β (π§ β π β βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β))) |
118 | 93, 117 | sylbird 260 |
. . . 4
β’ ((π β§ πΉ:πβontoβπ) β (π§ β (BaseβπΆ) β βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β))) |
119 | 118 | ralrimiv 3139 |
. . 3
β’ ((π β§ πΉ:πβontoβπ) β βπ§ β (BaseβπΆ)βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)) |
120 | 1, 2, 3, 4, 8, 11,
13 | isepi2 17629 |
. . . 4
β’ (π β (πΉ β (ππΈπ) β (πΉ β (π(Hom βπΆ)π) β§ βπ§ β (BaseβπΆ)βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)))) |
121 | 120 | adantr 482 |
. . 3
β’ ((π β§ πΉ:πβontoβπ) β (πΉ β (ππΈπ) β (πΉ β (π(Hom βπΆ)π) β§ βπ§ β (BaseβπΆ)βπ β (π(Hom βπΆ)π§)ββ β (π(Hom βπΆ)π§)((π(β¨π, πβ©(compβπΆ)π§)πΉ) = (β(β¨π, πβ©(compβπΆ)π§)πΉ) β π = β)))) |
122 | 91, 119, 121 | mpbir2and 712 |
. 2
β’ ((π β§ πΉ:πβontoβπ) β πΉ β (ππΈπ)) |
123 | 87, 122 | impbida 800 |
1
β’ (π β (πΉ β (ππΈπ) β πΉ:πβontoβπ)) |