This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- B = ( Base ` C )
catcocl.h 
|- H = ( Hom ` C )
catcocl.o 
|- .x. = ( comp ` C )
catcocl.c 
|- ( ph -> C e. Cat )
catcocl.x 
|- ( ph -> X e. B )
catcocl.y 
|- ( ph -> Y e. B )
catcocl.z 
|- ( ph -> Z e. B )
catcone0.f 
|- ( ph -> ( X H Y ) =/= (/) )
catcone0.g 
|- ( ph -> ( Y H Z ) =/= (/) )
Assertion catcone0 
|- ( ph -> ( X H Z ) =/= (/) )

Proof

Step Hyp Ref Expression
1 catcocl.b 
 |-  B = ( Base ` C )
2 catcocl.h 
 |-  H = ( Hom ` C )
3 catcocl.o 
 |-  .x. = ( comp ` C )
4 catcocl.c 
 |-  ( ph -> C e. Cat )
5 catcocl.x 
 |-  ( ph -> X e. B )
6 catcocl.y 
 |-  ( ph -> Y e. B )
7 catcocl.z 
 |-  ( ph -> Z e. B )
8 catcone0.f 
 |-  ( ph -> ( X H Y ) =/= (/) )
9 catcone0.g 
 |-  ( ph -> ( Y H Z ) =/= (/) )
10 n0 
 |-  ( ( X H Y ) =/= (/) <-> E. f f e. ( X H Y ) )
11 n0 
 |-  ( ( Y H Z ) =/= (/) <-> E. g g e. ( Y H Z ) )
12 10 11 anbi12i 
 |-  ( ( ( X H Y ) =/= (/) /\ ( Y H Z ) =/= (/) ) <-> ( E. f f e. ( X H Y ) /\ E. g g e. ( Y H Z ) ) )
13 exdistrv 
 |-  ( E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) <-> ( E. f f e. ( X H Y ) /\ E. g g e. ( Y H Z ) ) )
14 12 13 sylbb2 
 |-  ( ( ( X H Y ) =/= (/) /\ ( Y H Z ) =/= (/) ) -> E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) )
15 8 9 14 syl2anc 
 |-  ( ph -> E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) )
16 15 ancli 
 |-  ( ph -> ( ph /\ E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) )
17 19.42vv 
 |-  ( E. f E. g ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) <-> ( ph /\ E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) )
18 17 biimpri 
 |-  ( ( ph /\ E. f E. g ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> E. f E. g ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) )
19 4 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> C e. Cat )
20 5 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> X e. B )
21 6 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> Y e. B )
22 7 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> Z e. B )
23 simprl 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> f e. ( X H Y ) )
24 simprr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> g e. ( Y H Z ) )
25 1 2 3 19 20 21 22 23 24 catcocl 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> ( g ( <. X , Y >. .x. Z ) f ) e. ( X H Z ) )
26 25 2eximi 
 |-  ( E. f E. g ( ph /\ ( f e. ( X H Y ) /\ g e. ( Y H Z ) ) ) -> E. f E. g ( g ( <. X , Y >. .x. Z ) f ) e. ( X H Z ) )
27 ne0i 
 |-  ( ( g ( <. X , Y >. .x. Z ) f ) e. ( X H Z ) -> ( X H Z ) =/= (/) )
28 27 exlimivv 
 |-  ( E. f E. g ( g ( <. X , Y >. .x. Z ) f ) e. ( X H Z ) -> ( X H Z ) =/= (/) )
29 16 18 26 28 4syl 
 |-  ( ph -> ( X H Z ) =/= (/) )