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 ne0i ⊢ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ∈ ( 𝑋 𝐻 𝑍 ) → ( 𝑋 𝐻 𝑍 ) ≠ ∅ )
28 27 exlimivv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ∈ ( 𝑋 𝐻 𝑍 ) → ( 𝑋 𝐻 𝑍 ) ≠ ∅ )
29 16 18 26 28 4syl ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑍 ) ≠ ∅ )