Metamath Proof Explorer


Theorem catcone0

Description: Composition of non-empty hom-sets is non-empty. (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses catcocl.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
catcocl.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
catcocl.o โŠข ยท = ( comp โ€˜ ๐ถ )
catcocl.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
catcocl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
catcocl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
catcocl.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐ต )
catcone0.f โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ๐ป ๐‘Œ ) โ‰  โˆ… )
catcone0.g โŠข ( ๐œ‘ โ†’ ( ๐‘Œ ๐ป ๐‘ ) โ‰  โˆ… )
Assertion catcone0 ( ๐œ‘ โ†’ ( ๐‘‹ ๐ป ๐‘ ) โ‰  โˆ… )

Proof

Step Hyp Ref Expression
1 catcocl.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
2 catcocl.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
3 catcocl.o โŠข ยท = ( comp โ€˜ ๐ถ )
4 catcocl.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
5 catcocl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
6 catcocl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
7 catcocl.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐ต )
8 catcone0.f โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ๐ป ๐‘Œ ) โ‰  โˆ… )
9 catcone0.g โŠข ( ๐œ‘ โ†’ ( ๐‘Œ ๐ป ๐‘ ) โ‰  โˆ… )
10 n0 โŠข ( ( ๐‘‹ ๐ป ๐‘Œ ) โ‰  โˆ… โ†” โˆƒ ๐‘“ ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) )
11 n0 โŠข ( ( ๐‘Œ ๐ป ๐‘ ) โ‰  โˆ… โ†” โˆƒ ๐‘” ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) )
12 10 11 anbi12i โŠข ( ( ( ๐‘‹ ๐ป ๐‘Œ ) โ‰  โˆ… โˆง ( ๐‘Œ ๐ป ๐‘ ) โ‰  โˆ… ) โ†” ( โˆƒ ๐‘“ ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆƒ ๐‘” ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) )
13 exdistrv โŠข ( โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) โ†” ( โˆƒ ๐‘“ ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง โˆƒ ๐‘” ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) )
14 12 13 sylbb2 โŠข ( ( ( ๐‘‹ ๐ป ๐‘Œ ) โ‰  โˆ… โˆง ( ๐‘Œ ๐ป ๐‘ ) โ‰  โˆ… ) โ†’ โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) )
15 8 9 14 syl2anc โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) )
16 15 ancli โŠข ( ๐œ‘ โ†’ ( ๐œ‘ โˆง โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) )
17 19.42vv โŠข ( โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†” ( ๐œ‘ โˆง โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) )
18 17 biimpri โŠข ( ( ๐œ‘ โˆง โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) )
19 4 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐ถ โˆˆ Cat )
20 5 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
21 6 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐‘Œ โˆˆ ๐ต )
22 7 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐‘ โˆˆ ๐ต )
23 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) )
24 simprr โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) )
25 1 2 3 19 20 21 22 23 24 catcocl โŠข ( ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐‘“ ) โˆˆ ( ๐‘‹ ๐ป ๐‘ ) )
26 25 2eximi โŠข ( โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐œ‘ โˆง ( ๐‘“ โˆˆ ( ๐‘‹ ๐ป ๐‘Œ ) โˆง ๐‘” โˆˆ ( ๐‘Œ ๐ป ๐‘ ) ) ) โ†’ โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐‘“ ) โˆˆ ( ๐‘‹ ๐ป ๐‘ ) )
27 16 18 26 3syl โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐‘“ ) โˆˆ ( ๐‘‹ ๐ป ๐‘ ) )
28 ne0i โŠข ( ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐‘“ ) โˆˆ ( ๐‘‹ ๐ป ๐‘ ) โ†’ ( ๐‘‹ ๐ป ๐‘ ) โ‰  โˆ… )
29 28 exlimivv โŠข ( โˆƒ ๐‘“ โˆƒ ๐‘” ( ๐‘” ( โŸจ ๐‘‹ , ๐‘Œ โŸฉ ยท ๐‘ ) ๐‘“ ) โˆˆ ( ๐‘‹ ๐ป ๐‘ ) โ†’ ( ๐‘‹ ๐ป ๐‘ ) โ‰  โˆ… )
30 27 29 syl โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ๐ป ๐‘ ) โ‰  โˆ… )