fucof21

Description: The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fucof21.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fucof21.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucof21.j	$⊢ J = Hom (T)$
	fucof21.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
	fucof21.u	$⊢ φ \to U \in W$
	fucof21.v	$⊢ φ \to V \in W$
Assertion	fucof21	$⊢ φ \to (U P V) : U J V ⟶ O (U) (C Nat E) O (V)$

Proof

Step	Hyp	Ref	Expression
1		fucof21.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
2		fucof21.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
3		fucof21.j	$⊢ J = Hom (T)$
4		fucof21.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
5		fucof21.u	$⊢ φ \to U \in W$
6		fucof21.v	$⊢ φ \to V \in W$
7		relfunc	$⊢ Rel (D Func E)$
8		relfunc	$⊢ Rel (C Func D)$
9	4 5 7 8	fuco2eld3	$⊢ φ \to (1^{st} (1^{st} (U)) (D Func E) 2^{nd} (1^{st} (U)) \land 1^{st} (2^{nd} (U)) (C Func D) 2^{nd} (2^{nd} (U)))$
10	9	simprd	$⊢ φ \to 1^{st} (2^{nd} (U)) (C Func D) 2^{nd} (2^{nd} (U))$
11	9	simpld	$⊢ φ \to 1^{st} (1^{st} (U)) (D Func E) 2^{nd} (1^{st} (U))$
12	4 5 7 8	fuco2eld2	$⊢ φ \to U = ⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩$
13	4 6 7 8	fuco2eld3	$⊢ φ \to (1^{st} (1^{st} (V)) (D Func E) 2^{nd} (1^{st} (V)) \land 1^{st} (2^{nd} (V)) (C Func D) 2^{nd} (2^{nd} (V)))$
14	13	simprd	$⊢ φ \to 1^{st} (2^{nd} (V)) (C Func D) 2^{nd} (2^{nd} (V))$
15	13	simpld	$⊢ φ \to 1^{st} (1^{st} (V)) (D Func E) 2^{nd} (1^{st} (V))$
16	4 6 7 8	fuco2eld2	$⊢ φ \to V = ⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩$
17	1 10 11 12 14 15 16	fuco21	$⊢ φ \to U P V = (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩), a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩) ⟼ (x \in {Base}_{C} ⟼ b (1^{st} (2^{nd} (V)) (x)) (⟨1^{st} (1^{st} (U)) (1^{st} (2^{nd} (U)) (x)), 1^{st} (1^{st} (U)) (1^{st} (2^{nd} (V)) (x))⟩ comp (E) 1^{st} (1^{st} (V)) (1^{st} (2^{nd} (V)) (x))) (1^{st} (2^{nd} (U)) (x) 2^{nd} (1^{st} (U)) 1^{st} (2^{nd} (V)) (x)) (a (x))))$
18	1	adantr	Could not format ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
19	12	adantr	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to U = ⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩$
20	16	adantr	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to V = ⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩$
21		simprr	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩)$
22		simprl	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩)$
23	18 19 20 21 22	fuco22	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to b (U P V) a = (x \in {Base}_{C} ⟼ b (1^{st} (2^{nd} (V)) (x)) (⟨1^{st} (1^{st} (U)) (1^{st} (2^{nd} (U)) (x)), 1^{st} (1^{st} (U)) (1^{st} (2^{nd} (V)) (x))⟩ comp (E) 1^{st} (1^{st} (V)) (1^{st} (2^{nd} (V)) (x))) (1^{st} (2^{nd} (U)) (x) 2^{nd} (1^{st} (U)) 1^{st} (2^{nd} (V)) (x)) (a (x)))$
24	18 21 22 19 20	fuco22nat	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to b (U P V) a \in (O (U) (C Nat E) O (V))$
25	23 24	eqeltrrd	$⊢ (φ \land (b \in (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \land a \in (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩))) \to (x \in {Base}_{C} ⟼ b (1^{st} (2^{nd} (V)) (x)) (⟨1^{st} (1^{st} (U)) (1^{st} (2^{nd} (U)) (x)), 1^{st} (1^{st} (U)) (1^{st} (2^{nd} (V)) (x))⟩ comp (E) 1^{st} (1^{st} (V)) (1^{st} (2^{nd} (V)) (x))) (1^{st} (2^{nd} (U)) (x) 2^{nd} (1^{st} (U)) 1^{st} (2^{nd} (V)) (x)) (a (x))) \in (O (U) (C Nat E) O (V))$
26	2	xpcfucbas	$⊢ (D Func E) \times (C Func D) = {Base}_{T}$
27	5 4	eleqtrd	$⊢ φ \to U \in ((D Func E) \times (C Func D))$
28	6 4	eleqtrd	$⊢ φ \to V \in ((D Func E) \times (C Func D))$
29	2 26 3 27 28	xpcfuchom	$⊢ φ \to U J V = (1^{st} (U) (D Nat E) 1^{st} (V)) \times (2^{nd} (U) (C Nat D) 2^{nd} (V))$
30	12	fveq2d	$⊢ φ \to 1^{st} (U) = 1^{st} (⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩)$
31		opex	$⊢ ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ \in V$
32		opex	$⊢ ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ \in V$
33	31 32	op1st	$⊢ 1^{st} (⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩) = ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩$
34	30 33	eqtrdi	$⊢ φ \to 1^{st} (U) = ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩$
35	16	fveq2d	$⊢ φ \to 1^{st} (V) = 1^{st} (⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩)$
36		opex	$⊢ ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩ \in V$
37		opex	$⊢ ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩ \in V$
38	36 37	op1st	$⊢ 1^{st} (⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩) = ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩$
39	35 38	eqtrdi	$⊢ φ \to 1^{st} (V) = ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩$
40	34 39	oveq12d	$⊢ φ \to 1^{st} (U) (D Nat E) 1^{st} (V) = ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩$
41	12	fveq2d	$⊢ φ \to 2^{nd} (U) = 2^{nd} (⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩)$
42	31 32	op2nd	$⊢ 2^{nd} (⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩) = ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩$
43	41 42	eqtrdi	$⊢ φ \to 2^{nd} (U) = ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩$
44	16	fveq2d	$⊢ φ \to 2^{nd} (V) = 2^{nd} (⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩)$
45	36 37	op2nd	$⊢ 2^{nd} (⟨⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩, ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩⟩) = ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩$
46	44 45	eqtrdi	$⊢ φ \to 2^{nd} (V) = ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩$
47	43 46	oveq12d	$⊢ φ \to 2^{nd} (U) (C Nat D) 2^{nd} (V) = ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩$
48	40 47	xpeq12d	$⊢ φ \to (1^{st} (U) (D Nat E) 1^{st} (V)) \times (2^{nd} (U) (C Nat D) 2^{nd} (V)) = (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \times (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩)$
49	29 48	eqtrd	$⊢ φ \to U J V = (⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩ (D Nat E) ⟨1^{st} (1^{st} (V)), 2^{nd} (1^{st} (V))⟩) \times (⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩ (C Nat D) ⟨1^{st} (2^{nd} (V)), 2^{nd} (2^{nd} (V))⟩)$
50	17 25 49	fmpodg	$⊢ φ \to (U P V) : U J V ⟶ O (U) (C Nat E) O (V)$

Metamath Proof Explorer

Theorem fucof21

Proof