MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  catcone0 Structured version   Visualization version   GIF version

Theorem catcone0 17730
Description: Composition of non-empty hom-sets is non-empty. (Contributed by Zhi Wang, 18-Sep-2024.)
Hypotheses
Ref Expression
catcocl.b 𝐵 = (Base‘𝐶)
catcocl.h 𝐻 = (Hom ‘𝐶)
catcocl.o · = (comp‘𝐶)
catcocl.c (𝜑𝐶 ∈ Cat)
catcocl.x (𝜑𝑋𝐵)
catcocl.y (𝜑𝑌𝐵)
catcocl.z (𝜑𝑍𝐵)
catcone0.f (𝜑 → (𝑋𝐻𝑌) ≠ ∅)
catcone0.g (𝜑 → (𝑌𝐻𝑍) ≠ ∅)
Assertion
Ref Expression
catcone0 (𝜑 → (𝑋𝐻𝑍) ≠ ∅)

Proof of Theorem catcone0
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcone0.f . . . 4 (𝜑 → (𝑋𝐻𝑌) ≠ ∅)
2 catcone0.g . . . 4 (𝜑 → (𝑌𝐻𝑍) ≠ ∅)
3 n0 4353 . . . . . 6 ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑋𝐻𝑌))
4 n0 4353 . . . . . 6 ((𝑌𝐻𝑍) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍))
53, 4anbi12i 628 . . . . 5 (((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑍) ≠ ∅) ↔ (∃𝑓 𝑓 ∈ (𝑋𝐻𝑌) ∧ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍)))
6 exdistrv 1955 . . . . 5 (∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)) ↔ (∃𝑓 𝑓 ∈ (𝑋𝐻𝑌) ∧ ∃𝑔 𝑔 ∈ (𝑌𝐻𝑍)))
75, 6sylbb2 238 . . . 4 (((𝑋𝐻𝑌) ≠ ∅ ∧ (𝑌𝐻𝑍) ≠ ∅) → ∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)))
81, 2, 7syl2anc 584 . . 3 (𝜑 → ∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍)))
98ancli 548 . 2 (𝜑 → (𝜑 ∧ ∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))))
10 19.42vv 1957 . . 3 (∃𝑓𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) ↔ (𝜑 ∧ ∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))))
1110biimpri 228 . 2 ((𝜑 ∧ ∃𝑓𝑔(𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → ∃𝑓𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))))
12 catcocl.b . . . 4 𝐵 = (Base‘𝐶)
13 catcocl.h . . . 4 𝐻 = (Hom ‘𝐶)
14 catcocl.o . . . 4 · = (comp‘𝐶)
15 catcocl.c . . . . 5 (𝜑𝐶 ∈ Cat)
1615adantr 480 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝐶 ∈ Cat)
17 catcocl.x . . . . 5 (𝜑𝑋𝐵)
1817adantr 480 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑋𝐵)
19 catcocl.y . . . . 5 (𝜑𝑌𝐵)
2019adantr 480 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑌𝐵)
21 catcocl.z . . . . 5 (𝜑𝑍𝐵)
2221adantr 480 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑍𝐵)
23 simprl 771 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑓 ∈ (𝑋𝐻𝑌))
24 simprr 773 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → 𝑔 ∈ (𝑌𝐻𝑍))
2512, 13, 14, 16, 18, 20, 22, 23, 24catcocl 17728 . . 3 ((𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → (𝑔(⟨𝑋, 𝑌· 𝑍)𝑓) ∈ (𝑋𝐻𝑍))
26252eximi 1836 . 2 (∃𝑓𝑔(𝜑 ∧ (𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑍))) → ∃𝑓𝑔(𝑔(⟨𝑋, 𝑌· 𝑍)𝑓) ∈ (𝑋𝐻𝑍))
27 ne0i 4341 . . 3 ((𝑔(⟨𝑋, 𝑌· 𝑍)𝑓) ∈ (𝑋𝐻𝑍) → (𝑋𝐻𝑍) ≠ ∅)
2827exlimivv 1932 . 2 (∃𝑓𝑔(𝑔(⟨𝑋, 𝑌· 𝑍)𝑓) ∈ (𝑋𝐻𝑍) → (𝑋𝐻𝑍) ≠ ∅)
299, 11, 26, 284syl 19 1 (𝜑 → (𝑋𝐻𝑍) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wex 1779  wcel 2108  wne 2940  c0 4333  cop 4632  cfv 6561  (class class class)co 7431  Basecbs 17247  Hom chom 17308  compcco 17309  Catccat 17707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-cat 17711
This theorem is referenced by:  catprs  48900
  Copyright terms: Public domain W3C validator