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

Theorem hof2fval 18220
Description: The morphism part of the Hom functor, for morphisms βŸ¨π‘“, π‘”βŸ©:βŸ¨π‘‹, π‘ŒβŸ©βŸΆβŸ¨π‘, π‘ŠβŸ© (which since the first argument is contravariant means morphisms 𝑓:π‘βŸΆπ‘‹ and 𝑔:π‘ŒβŸΆπ‘Š), yields a function (a morphism of SetCat) mapping β„Ž:π‘‹βŸΆπ‘Œ to 𝑔 ∘ β„Ž ∘ 𝑓:π‘βŸΆπ‘Š. (Contributed by Mario Carneiro, 15-Jan-2017.)
Hypotheses
Ref Expression
hofval.m 𝑀 = (HomFβ€˜πΆ)
hofval.c (πœ‘ β†’ 𝐢 ∈ Cat)
hof1.b 𝐡 = (Baseβ€˜πΆ)
hof1.h 𝐻 = (Hom β€˜πΆ)
hof1.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
hof1.y (πœ‘ β†’ π‘Œ ∈ 𝐡)
hof2.z (πœ‘ β†’ 𝑍 ∈ 𝐡)
hof2.w (πœ‘ β†’ π‘Š ∈ 𝐡)
hof2.o Β· = (compβ€˜πΆ)
Assertion
Ref Expression
hof2fval (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ©(2nd β€˜π‘€)βŸ¨π‘, π‘ŠβŸ©) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))))
Distinct variable groups:   𝑓,𝑔,β„Ž,𝐡   πœ‘,𝑓,𝑔,β„Ž   𝐢,𝑓,𝑔,β„Ž   𝑓,𝐻,𝑔,β„Ž   𝑓,π‘Š,𝑔,β„Ž   Β· ,𝑓,𝑔,β„Ž   𝑓,𝑋,𝑔,β„Ž   𝑓,π‘Œ,𝑔,β„Ž   𝑓,𝑍,𝑔,β„Ž
Allowed substitution hints:   𝑀(𝑓,𝑔,β„Ž)

Proof of Theorem hof2fval
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofval.m . . . 4 𝑀 = (HomFβ€˜πΆ)
2 hofval.c . . . 4 (πœ‘ β†’ 𝐢 ∈ Cat)
3 hof1.b . . . 4 𝐡 = (Baseβ€˜πΆ)
4 hof1.h . . . 4 𝐻 = (Hom β€˜πΆ)
5 hof2.o . . . 4 Β· = (compβ€˜πΆ)
61, 2, 3, 4, 5hofval 18217 . . 3 (πœ‘ β†’ 𝑀 = ⟨(Homf β€˜πΆ), (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))))⟩)
7 fvex 6898 . . . 4 (Homf β€˜πΆ) ∈ V
83fvexi 6899 . . . . . 6 𝐡 ∈ V
98, 8xpex 7737 . . . . 5 (𝐡 Γ— 𝐡) ∈ V
109, 9mpoex 8065 . . . 4 (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)))) ∈ V
117, 10op2ndd 7985 . . 3 (𝑀 = ⟨(Homf β€˜πΆ), (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))))⟩ β†’ (2nd β€˜π‘€) = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)))))
126, 11syl 17 . 2 (πœ‘ β†’ (2nd β€˜π‘€) = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)))))
13 simprr 770 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)
1413fveq2d 6889 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘¦) = (1st β€˜βŸ¨π‘, π‘ŠβŸ©))
15 hof2.z . . . . . . 7 (πœ‘ β†’ 𝑍 ∈ 𝐡)
16 hof2.w . . . . . . 7 (πœ‘ β†’ π‘Š ∈ 𝐡)
17 op1stg 7986 . . . . . . 7 ((𝑍 ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
1815, 16, 17syl2anc 583 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
1918adantr 480 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
2014, 19eqtrd 2766 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘¦) = 𝑍)
21 simprl 768 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ π‘₯ = βŸ¨π‘‹, π‘ŒβŸ©)
2221fveq2d 6889 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©))
23 hof1.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐡)
24 hof1.y . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ 𝐡)
25 op1stg 7986 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2623, 24, 25syl2anc 583 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2726adantr 480 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2822, 27eqtrd 2766 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘₯) = 𝑋)
2920, 28oveq12d 7423 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)) = (𝑍𝐻𝑋))
3021fveq2d 6889 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©))
31 op2ndg 7987 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3223, 24, 31syl2anc 583 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3332adantr 480 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3430, 33eqtrd 2766 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘₯) = π‘Œ)
3513fveq2d 6889 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘¦) = (2nd β€˜βŸ¨π‘, π‘ŠβŸ©))
36 op2ndg 7987 . . . . . . 7 ((𝑍 ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3715, 16, 36syl2anc 583 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3837adantr 480 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3935, 38eqtrd 2766 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘¦) = π‘Š)
4034, 39oveq12d 7423 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) = (π‘Œπ»π‘Š))
4121fveq2d 6889 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π»β€˜π‘₯) = (π»β€˜βŸ¨π‘‹, π‘ŒβŸ©))
42 df-ov 7408 . . . . 5 (π‘‹π»π‘Œ) = (π»β€˜βŸ¨π‘‹, π‘ŒβŸ©)
4341, 42eqtr4di 2784 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π»β€˜π‘₯) = (π‘‹π»π‘Œ))
4420, 28opeq12d 4876 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ = βŸ¨π‘, π‘‹βŸ©)
4544, 39oveq12d 7423 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦)) = (βŸ¨π‘, π‘‹βŸ© Β· π‘Š))
4621, 39oveq12d 7423 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π‘₯ Β· (2nd β€˜π‘¦)) = (βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š))
4746oveqd 7422 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž) = (𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž))
48 eqidd 2727 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ 𝑓 = 𝑓)
4945, 47, 48oveq123d 7426 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓) = ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))
5043, 49mpteq12dv 5232 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)) = (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓)))
5129, 40, 50mpoeq123dv 7480 . 2 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))))
5223, 24opelxpd 5708 . 2 (πœ‘ β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ (𝐡 Γ— 𝐡))
5315, 16opelxpd 5708 . 2 (πœ‘ β†’ βŸ¨π‘, π‘ŠβŸ© ∈ (𝐡 Γ— 𝐡))
54 ovex 7438 . . . 4 (𝑍𝐻𝑋) ∈ V
55 ovex 7438 . . . 4 (π‘Œπ»π‘Š) ∈ V
5654, 55mpoex 8065 . . 3 (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))) ∈ V
5756a1i 11 . 2 (πœ‘ β†’ (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))) ∈ V)
5812, 51, 52, 53, 57ovmpod 7556 1 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ©(2nd β€˜π‘€)βŸ¨π‘, π‘ŠβŸ©) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  Vcvv 3468  βŸ¨cop 4629   ↦ cmpt 5224   Γ— cxp 5667  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  1st c1st 7972  2nd c2nd 7973  Basecbs 17153  Hom chom 17217  compcco 17218  Catccat 17617  Homf chomf 17619  HomFchof 18213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7974  df-2nd 7975  df-hof 18215
This theorem is referenced by:  hof2val  18221
  Copyright terms: Public domain W3C validator