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	$⊢ \underset{˙}{\cdot} = comp (C)$
	catcocl.c	$⊢ φ \to C \in Cat$
	catcocl.x	$⊢ φ \to X \in B$
	catcocl.y	$⊢ φ \to Y \in B$
	catcocl.z	$⊢ φ \to Z \in B$
	catcone0.f	$⊢ φ \to X H Y \neq \emptyset$
	catcone0.g	$⊢ φ \to Y H Z \neq \emptyset$
Assertion	catcone0	$⊢ φ \to X H Z \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		catcocl.b	$⊢ B = {Base}_{C}$
2		catcocl.h	$⊢ H = Hom (C)$
3		catcocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		catcocl.c	$⊢ φ \to C \in Cat$
5		catcocl.x	$⊢ φ \to X \in B$
6		catcocl.y	$⊢ φ \to Y \in B$
7		catcocl.z	$⊢ φ \to Z \in B$
8		catcone0.f	$⊢ φ \to X H Y \neq \emptyset$
9		catcone0.g	$⊢ φ \to Y H Z \neq \emptyset$
10		n0	$⊢ X H Y \neq \emptyset \leftrightarrow \exists f f \in (X H Y)$
11		n0	$⊢ Y H Z \neq \emptyset \leftrightarrow \exists g g \in (Y H Z)$
12	10 11	anbi12i	$⊢ (X H Y \neq \emptyset \land Y H Z \neq \emptyset) \leftrightarrow (\exists f f \in (X H Y) \land \exists g g \in (Y H Z))$
13		exdistrv	$⊢ \exists f \exists g (f \in (X H Y) \land g \in (Y H Z)) \leftrightarrow (\exists f f \in (X H Y) \land \exists g g \in (Y H Z))$
14	12 13	sylbb2	$⊢ (X H Y \neq \emptyset \land Y H Z \neq \emptyset) \to \exists f \exists g (f \in (X H Y) \land g \in (Y H Z))$
15	8 9 14	syl2anc	$⊢ φ \to \exists f \exists g (f \in (X H Y) \land g \in (Y H Z))$
16	15	ancli	$⊢ φ \to (φ \land \exists f \exists g (f \in (X H Y) \land g \in (Y H Z)))$
17		19.42vv	$⊢ \exists f \exists g (φ \land (f \in (X H Y) \land g \in (Y H Z))) \leftrightarrow (φ \land \exists f \exists g (f \in (X H Y) \land g \in (Y H Z)))$
18	17	biimpri	$⊢ (φ \land \exists f \exists g (f \in (X H Y) \land g \in (Y H Z))) \to \exists f \exists g (φ \land (f \in (X H Y) \land g \in (Y H Z)))$
19	4	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to C \in Cat$
20	5	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to X \in B$
21	6	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to Y \in B$
22	7	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to Z \in B$
23		simprl	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to f \in (X H Y)$
24		simprr	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to g \in (Y H Z)$
25	1 2 3 19 20 21 22 23 24	catcocl	$⊢ (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f \in (X H Z)$
26	25	2eximi	$⊢ \exists f \exists g (φ \land (f \in (X H Y) \land g \in (Y H Z))) \to \exists f \exists g g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f \in (X H Z)$
27		ne0i	$⊢ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f \in (X H Z) \to X H Z \neq \emptyset$
28	27	exlimivv	$⊢ \exists f \exists g g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f \in (X H Z) \to X H Z \neq \emptyset$
29	16 18 26 28	4syl	$⊢ φ \to X H Z \neq \emptyset$

Metamath Proof Explorer

Theorem catcone0

Proof