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

Theorem catcocl 17700
Description: Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catcocl.b 𝐵 = (Base‘𝐶)
catcocl.h 𝐻 = (Hom ‘𝐶)
catcocl.o · = (comp‘𝐶)
catcocl.c (𝜑𝐶 ∈ Cat)
catcocl.x (𝜑𝑋𝐵)
catcocl.y (𝜑𝑌𝐵)
catcocl.z (𝜑𝑍𝐵)
catcocl.f (𝜑𝐹 ∈ (𝑋𝐻𝑌))
catcocl.g (𝜑𝐺 ∈ (𝑌𝐻𝑍))
Assertion
Ref Expression
catcocl (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Proof of Theorem catcocl
Dummy variables 𝑓 𝑔 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcocl.c . . 3 (𝜑𝐶 ∈ Cat)
2 catcocl.b . . . . 5 𝐵 = (Base‘𝐶)
3 catcocl.h . . . . 5 𝐻 = (Hom ‘𝐶)
4 catcocl.o . . . . 5 · = (comp‘𝐶)
52, 3, 4iscat 17687 . . . 4 (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
65ibi 266 . . 3 (𝐶 ∈ Cat → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
7 simpl 481 . . . . . . 7 (((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
872ralimi 3113 . . . . . 6 (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
982ralimi 3113 . . . . 5 (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
109adantl 480 . . . 4 ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
1110ralimi 3073 . . 3 (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
121, 6, 113syl 18 . 2 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
13 catcocl.x . . 3 (𝜑𝑋𝐵)
14 catcocl.y . . . . 5 (𝜑𝑌𝐵)
1514adantr 479 . . . 4 ((𝜑𝑥 = 𝑋) → 𝑌𝐵)
16 catcocl.z . . . . . 6 (𝜑𝑍𝐵)
1716ad2antrr 724 . . . . 5 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍𝐵)
18 catcocl.f . . . . . . . 8 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
1918ad3antrrr 728 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌))
20 simpllr 774 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
21 simplr 767 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
2220, 21oveq12d 7444 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
2319, 22eleqtrrd 2829 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦))
24 catcocl.g . . . . . . . . . 10 (𝜑𝐺 ∈ (𝑌𝐻𝑍))
2524ad3antrrr 728 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑌𝐻𝑍))
26 simpr 483 . . . . . . . . . 10 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
2721, 26oveq12d 7444 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
2825, 27eleqtrrd 2829 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑦𝐻𝑧))
2928adantr 479 . . . . . . 7 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧))
30 simp-5r 784 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑥 = 𝑋)
31 simp-4r 782 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑦 = 𝑌)
3230, 31opeq12d 4889 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
33 simpllr 774 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑧 = 𝑍)
3432, 33oveq12d 7444 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑋, 𝑌· 𝑍))
35 simpr 483 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
36 simplr 767 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
3734, 35, 36oveq123d 7447 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))
3830, 33oveq12d 7444 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥𝐻𝑧) = (𝑋𝐻𝑍))
3937, 38eleq12d 2820 . . . . . . 7 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4029, 39rspcdv 3600 . . . . . 6 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4123, 40rspcimdv 3598 . . . . 5 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4217, 41rspcimdv 3598 . . . 4 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4315, 42rspcimdv 3598 . . 3 ((𝜑𝑥 = 𝑋) → (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4413, 43rspcimdv 3598 . 2 (𝜑 → (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4512, 44mpd 15 1 (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wral 3051  wrex 3060  cop 4639  cfv 6556  (class class class)co 7426  Basecbs 17215  Hom chom 17279  compcco 17280  Catccat 17679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5313
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-iota 6508  df-fv 6564  df-ov 7429  df-cat 17683
This theorem is referenced by:  catcone0  17702  oppccatid  17736  ismon2  17752  isepi2  17759  sectco  17774  monsect  17801  catsubcat  17860  issubc3  17870  fullsubc  17871  idfucl  17902  cofucl  17909  fthsect  17949  fthmon  17951  fuccocl  17991  invfuc  18001  2initoinv  18034  initoeu2lem0  18037  initoeu2lem1  18038  initoeu2  18040  2termoinv  18041  coahom  18094  catcisolem  18134  xpccatid  18214  1stfcl  18223  2ndfcl  18224  prfcl  18229  evlfcllem  18248  evlfcl  18249  curf1cl  18255  curfcl  18259  hofcllem  18285  hofcl  18286  yon12  18292  hofpropd  18294  yonedalem4c  18304  srhmsubc  20660  bj-endmnd  37027  srhmsubcALTV  47720  endmndlem  48354  functhinclem4  48383  thincsect  48396
  Copyright terms: Public domain W3C validator