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

Theorem cofu2nd 16941
 Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
Hypotheses
Ref Expression
cofuval.b 𝐵 = (Base‘𝐶)
cofuval.f (𝜑𝐹 ∈ (𝐶 Func 𝐷))
cofuval.g (𝜑𝐺 ∈ (𝐷 Func 𝐸))
cofu2nd.x (𝜑𝑋𝐵)
cofu2nd.y (𝜑𝑌𝐵)
Assertion
Ref Expression
cofu2nd (𝜑 → (𝑋(2nd ‘(𝐺func 𝐹))𝑌) = ((((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∘ (𝑋(2nd𝐹)𝑌)))

Proof of Theorem cofu2nd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cofuval.b . . . . 5 𝐵 = (Base‘𝐶)
2 cofuval.f . . . . 5 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
3 cofuval.g . . . . 5 (𝜑𝐺 ∈ (𝐷 Func 𝐸))
41, 2, 3cofuval 16938 . . . 4 (𝜑 → (𝐺func 𝐹) = ⟨((1st𝐺) ∘ (1st𝐹)), (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩)
54fveq2d 6452 . . 3 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩))
6 fvex 6461 . . . . 5 (1st𝐺) ∈ V
7 fvex 6461 . . . . 5 (1st𝐹) ∈ V
86, 7coex 7399 . . . 4 ((1st𝐺) ∘ (1st𝐹)) ∈ V
91fvexi 6462 . . . . 5 𝐵 ∈ V
109, 9mpt2ex 7529 . . . 4 (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))) ∈ V
118, 10op2nd 7456 . . 3 (2nd ‘⟨((1st𝐺) ∘ (1st𝐹)), (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))⟩) = (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
125, 11syl6eq 2830 . 2 (𝜑 → (2nd ‘(𝐺func 𝐹)) = (𝑥𝐵, 𝑦𝐵 ↦ ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦))))
13 simprl 761 . . . . 5 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝑥 = 𝑋)
1413fveq2d 6452 . . . 4 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → ((1st𝐹)‘𝑥) = ((1st𝐹)‘𝑋))
15 simprr 763 . . . . 5 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝑦 = 𝑌)
1615fveq2d 6452 . . . 4 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → ((1st𝐹)‘𝑦) = ((1st𝐹)‘𝑌))
1714, 16oveq12d 6942 . . 3 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → (((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) = (((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)))
1813, 15oveq12d 6942 . . 3 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → (𝑥(2nd𝐹)𝑦) = (𝑋(2nd𝐹)𝑌))
1917, 18coeq12d 5534 . 2 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → ((((1st𝐹)‘𝑥)(2nd𝐺)((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) = ((((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∘ (𝑋(2nd𝐹)𝑌)))
20 cofu2nd.x . 2 (𝜑𝑋𝐵)
21 cofu2nd.y . 2 (𝜑𝑌𝐵)
22 ovex 6956 . . . 4 (((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∈ V
23 ovex 6956 . . . 4 (𝑋(2nd𝐹)𝑌) ∈ V
2422, 23coex 7399 . . 3 ((((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∘ (𝑋(2nd𝐹)𝑌)) ∈ V
2524a1i 11 . 2 (𝜑 → ((((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∘ (𝑋(2nd𝐹)𝑌)) ∈ V)
2612, 19, 20, 21, 25ovmpt2d 7067 1 (𝜑 → (𝑋(2nd ‘(𝐺func 𝐹))𝑌) = ((((1st𝐹)‘𝑋)(2nd𝐺)((1st𝐹)‘𝑌)) ∘ (𝑋(2nd𝐹)𝑌)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  Vcvv 3398  ⟨cop 4404   ∘ ccom 5361  ‘cfv 6137  (class class class)co 6924   ↦ cmpt2 6926  1st c1st 7445  2nd c2nd 7446  Basecbs 16266   Func cfunc 16910   ∘func ccofu 16912 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-1st 7447  df-2nd 7448  df-map 8144  df-ixp 8197  df-func 16914  df-cofu 16916 This theorem is referenced by:  cofu2  16942  cofucl  16944  cofuass  16945  cofull  16990  cofth  16991  catciso  17153
 Copyright terms: Public domain W3C validator