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	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑍 ) ≠ ∅ )