Metamath Proof Explorer

Theorem isepi2

Description: Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
isepi.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
isepi.o โŠข ยท = ( comp โ€˜ ๐ถ )
isepi.e โŠข ๐ธ = ( Epi โ€˜ ๐ถ )
isepi.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
isepi.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
isepi.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
Assertion isepi2 ( ๐œ‘ โ†’ ( ๐น โˆˆ ( ๐‘‹ ๐ธ ๐‘Œ ) โ†” ( ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) ) )

Proof

Step Hyp Ref Expression
1 isepi.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
2 isepi.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
3 isepi.o โŠข ยท = ( comp โ€˜ ๐ถ )
4 isepi.e โŠข ๐ธ = ( Epi โ€˜ ๐ถ )
5 isepi.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
6 isepi.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
7 isepi.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
8 1 2 3 4 5 6 7 isepi โŠข ( ๐œ‘ โ†’ ( ๐น โˆˆ ( ๐‘‹ ๐ธ ๐‘Œ ) โ†” ( ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) ) ) )
9 5 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐ถ โˆˆ Cat )
10 6 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
11 7 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐‘Œ โˆˆ ๐ต )
12 simprl โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐‘ง โˆˆ ๐ต )
13 simplr โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) )
14 simprr โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) )
15 1 2 3 9 10 11 12 13 14 catcocl โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ( ๐‘ง โˆˆ ๐ต โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) ) โ†’ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) )
16 15 anassrs โŠข ( ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ๐‘ง โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ) โ†’ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) )
17 16 ralrimiva โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ๐‘ง โˆˆ ๐ต ) โ†’ โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) )
18 eqid โŠข ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) = ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) )
19 18 fmpt โŠข ( โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) โ†” ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โŸถ ( ๐‘‹ ๐ป ๐‘ง ) )
20 df-f1 โŠข ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โ€“1-1โ†’ ( ๐‘‹ ๐ป ๐‘ง ) โ†” ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โŸถ ( ๐‘‹ ๐ป ๐‘ง ) โˆง Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) ) )
21 20 baib โŠข ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โŸถ ( ๐‘‹ ๐ป ๐‘ง ) โ†’ ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โ€“1-1โ†’ ( ๐‘‹ ๐ป ๐‘ง ) โ†” Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) ) )
22 19 21 sylbi โŠข ( โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) โ†’ ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โ€“1-1โ†’ ( ๐‘‹ ๐ป ๐‘ง ) โ†” Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) ) )
23 oveq1 โŠข ( ๐‘” = โ„Ž โ†’ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) )
24 18 23 f1mpt โŠข ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โ€“1-1โ†’ ( ๐‘‹ ๐ป ๐‘ง ) โ†” ( โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) โˆง โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) )
25 24 baib โŠข ( โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) โ†’ ( ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) : ( ๐‘Œ ๐ป ๐‘ง ) โ€“1-1โ†’ ( ๐‘‹ ๐ป ๐‘ง ) โ†” โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) )
26 22 25 bitr3d โŠข ( โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โˆˆ ( ๐‘‹ ๐ป ๐‘ง ) โ†’ ( Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) โ†” โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) )
27 17 26 syl โŠข ( ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โˆง ๐‘ง โˆˆ ๐ต ) โ†’ ( Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) โ†” โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) )
28 27 ralbidva โŠข ( ( ๐œ‘ โˆง ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) ) โ†’ ( โˆ€ ๐‘ง โˆˆ ๐ต Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) โ†” โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) )
29 28 pm5.32da โŠข ( ๐œ‘ โ†’ ( ( ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต Fun โ—ก ( ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โ†ฆ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) ) ) โ†” ( ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) ) )
30 8 29 bitrd โŠข ( ๐œ‘ โ†’ ( ๐น โˆˆ ( ๐‘‹ ๐ธ ๐‘Œ ) โ†” ( ๐น โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) โˆ€ โ„Ž โˆˆ ( ๐‘Œ ๐ป ๐‘ง ) ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) = ( โ„Ž ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ง ) ๐น ) โ†’ ๐‘” = โ„Ž ) ) ) )