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

Theorem catcocl 17492
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 17479 . . . 4 (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
65ibi 266 . . 3 (𝐶 ∈ Cat → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
7 simpl 483 . . . . . . 7 (((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
872ralimi 3122 . . . . . 6 (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
982ralimi 3122 . . . . 5 (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
109adantl 482 . . . 4 ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
1110ralimi 3082 . . 3 (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑣 ∈ (𝑧𝐻𝑤)((𝑣(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑣(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
121, 6, 113syl 18 . 2 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
13 catcocl.x . . 3 (𝜑𝑋𝐵)
14 catcocl.y . . . . 5 (𝜑𝑌𝐵)
1514adantr 481 . . . 4 ((𝜑𝑥 = 𝑋) → 𝑌𝐵)
16 catcocl.z . . . . . 6 (𝜑𝑍𝐵)
1716ad2antrr 723 . . . . 5 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍𝐵)
18 catcocl.f . . . . . . . 8 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
1918ad3antrrr 727 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌))
20 simpllr 773 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
21 simplr 766 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
2220, 21oveq12d 7356 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
2319, 22eleqtrrd 2840 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦))
24 catcocl.g . . . . . . . . . 10 (𝜑𝐺 ∈ (𝑌𝐻𝑍))
2524ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑌𝐻𝑍))
26 simpr 485 . . . . . . . . . 10 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
2721, 26oveq12d 7356 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
2825, 27eleqtrrd 2840 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐺 ∈ (𝑦𝐻𝑧))
2928adantr 481 . . . . . . 7 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧))
30 simp-5r 783 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑥 = 𝑋)
31 simp-4r 781 . . . . . . . . . . 11 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑦 = 𝑌)
3230, 31opeq12d 4826 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
33 simpllr 773 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑧 = 𝑍)
3432, 33oveq12d 7356 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑋, 𝑌· 𝑍))
35 simpr 485 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
36 simplr 766 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
3734, 35, 36oveq123d 7359 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))
3830, 33oveq12d 7356 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥𝐻𝑧) = (𝑋𝐻𝑍))
3937, 38eleq12d 2831 . . . . . . 7 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4029, 39rspcdv 3562 . . . . . 6 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4123, 40rspcimdv 3560 . . . . 5 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4217, 41rspcimdv 3560 . . . 4 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4315, 42rspcimdv 3560 . . 3 ((𝜑𝑥 = 𝑋) → (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4413, 43rspcimdv 3560 . 2 (𝜑 → (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
4512, 44mpd 15 1 (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wral 3061  wrex 3070  cop 4580  cfv 6480  (class class class)co 7338  Basecbs 17010  Hom chom 17071  compcco 17072  Catccat 17471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-nul 5251
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-iota 6432  df-fv 6488  df-ov 7341  df-cat 17475
This theorem is referenced by:  catcone0  17494  oppccatid  17528  ismon2  17544  isepi2  17551  sectco  17566  monsect  17593  catsubcat  17652  issubc3  17662  fullsubc  17663  idfucl  17694  cofucl  17701  fthsect  17739  fthmon  17741  fuccocl  17780  invfuc  17790  2initoinv  17823  initoeu2lem0  17826  initoeu2lem1  17827  initoeu2  17829  2termoinv  17830  coahom  17883  catcisolem  17923  xpccatid  18003  1stfcl  18012  2ndfcl  18013  prfcl  18018  evlfcllem  18037  evlfcl  18038  curf1cl  18044  curfcl  18048  hofcllem  18074  hofcl  18075  yon12  18081  hofpropd  18083  yonedalem4c  18093  bj-endmnd  35645  srhmsubc  46052  srhmsubcALTV  46070  endmndlem  46714  functhinclem4  46743  thincsect  46756
  Copyright terms: Public domain W3C validator