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

Theorem hof2fval 18104
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 18101 . . 3 (πœ‘ β†’ 𝑀 = ⟨(Homf β€˜πΆ), (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))))⟩)
7 fvex 6852 . . . 4 (Homf β€˜πΆ) ∈ V
83fvexi 6853 . . . . . 6 𝐡 ∈ V
98, 8xpex 7679 . . . . 5 (𝐡 Γ— 𝐡) ∈ V
109, 9mpoex 8004 . . . 4 (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)))) ∈ V
117, 10op2ndd 7924 . . 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 771 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)
1413fveq2d 6843 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘¦) = (1st β€˜βŸ¨π‘, π‘ŠβŸ©))
15 hof2.z . . . . . . 7 (πœ‘ β†’ 𝑍 ∈ 𝐡)
16 hof2.w . . . . . . 7 (πœ‘ β†’ π‘Š ∈ 𝐡)
17 op1stg 7925 . . . . . . 7 ((𝑍 ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
1815, 16, 17syl2anc 584 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
1918adantr 481 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜βŸ¨π‘, π‘ŠβŸ©) = 𝑍)
2014, 19eqtrd 2777 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘¦) = 𝑍)
21 simprl 769 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ π‘₯ = βŸ¨π‘‹, π‘ŒβŸ©)
2221fveq2d 6843 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©))
23 hof1.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐡)
24 hof1.y . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ 𝐡)
25 op1stg 7925 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2623, 24, 25syl2anc 584 . . . . . 6 (πœ‘ β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2726adantr 481 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜βŸ¨π‘‹, π‘ŒβŸ©) = 𝑋)
2822, 27eqtrd 2777 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (1st β€˜π‘₯) = 𝑋)
2920, 28oveq12d 7369 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)) = (𝑍𝐻𝑋))
3021fveq2d 6843 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©))
31 op2ndg 7926 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3223, 24, 31syl2anc 584 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3332adantr 481 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜βŸ¨π‘‹, π‘ŒβŸ©) = π‘Œ)
3430, 33eqtrd 2777 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘₯) = π‘Œ)
3513fveq2d 6843 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘¦) = (2nd β€˜βŸ¨π‘, π‘ŠβŸ©))
36 op2ndg 7926 . . . . . . 7 ((𝑍 ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3715, 16, 36syl2anc 584 . . . . . 6 (πœ‘ β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3837adantr 481 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜βŸ¨π‘, π‘ŠβŸ©) = π‘Š)
3935, 38eqtrd 2777 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (2nd β€˜π‘¦) = π‘Š)
4034, 39oveq12d 7369 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) = (π‘Œπ»π‘Š))
4121fveq2d 6843 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π»β€˜π‘₯) = (π»β€˜βŸ¨π‘‹, π‘ŒβŸ©))
42 df-ov 7354 . . . . 5 (π‘‹π»π‘Œ) = (π»β€˜βŸ¨π‘‹, π‘ŒβŸ©)
4341, 42eqtr4di 2795 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π»β€˜π‘₯) = (π‘‹π»π‘Œ))
4420, 28opeq12d 4836 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ = βŸ¨π‘, π‘‹βŸ©)
4544, 39oveq12d 7369 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦)) = (βŸ¨π‘, π‘‹βŸ© Β· π‘Š))
4621, 39oveq12d 7369 . . . . . 6 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (π‘₯ Β· (2nd β€˜π‘¦)) = (βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š))
4746oveqd 7368 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž) = (𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž))
48 eqidd 2738 . . . . 5 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ 𝑓 = 𝑓)
4945, 47, 48oveq123d 7372 . . . 4 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓) = ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))
5043, 49mpteq12dv 5194 . . 3 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)) = (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓)))
5129, 40, 50mpoeq123dv 7426 . 2 ((πœ‘ ∧ (π‘₯ = βŸ¨π‘‹, π‘ŒβŸ© ∧ 𝑦 = βŸ¨π‘, π‘ŠβŸ©)) β†’ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))))
5223, 24opelxpd 5669 . 2 (πœ‘ β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ (𝐡 Γ— 𝐡))
5315, 16opelxpd 5669 . 2 (πœ‘ β†’ βŸ¨π‘, π‘ŠβŸ© ∈ (𝐡 Γ— 𝐡))
54 ovex 7384 . . . 4 (𝑍𝐻𝑋) ∈ V
55 ovex 7384 . . . 4 (π‘Œπ»π‘Š) ∈ V
5654, 55mpoex 8004 . . 3 (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))) ∈ V
5756a1i 11 . 2 (πœ‘ β†’ (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))) ∈ V)
5812, 51, 52, 53, 57ovmpod 7501 1 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ©(2nd β€˜π‘€)βŸ¨π‘, π‘ŠβŸ©) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (π‘Œπ»π‘Š) ↦ (β„Ž ∈ (π‘‹π»π‘Œ) ↦ ((𝑔(βŸ¨π‘‹, π‘ŒβŸ© Β· π‘Š)β„Ž)(βŸ¨π‘, π‘‹βŸ© Β· π‘Š)𝑓))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3443  βŸ¨cop 4590   ↦ cmpt 5186   Γ— cxp 5629  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353  1st c1st 7911  2nd c2nd 7912  Basecbs 17043  Hom chom 17104  compcco 17105  Catccat 17504  Homf chomf 17506  HomFchof 18097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-1st 7913  df-2nd 7914  df-hof 18099
This theorem is referenced by:  hof2val  18105
  Copyright terms: Public domain W3C validator