fuco22a

Description: The morphism part of the functor composition bifunctor. See also fuco22 . (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	fuco22a.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco22a.u	$⊢ φ \to U = ⟨K, F⟩$
	fuco22a.v	$⊢ φ \to V = ⟨R, M⟩$
	fuco22a.a	$⊢ φ \to A \in (F (C Nat D) M)$
	fuco22a.b	$⊢ φ \to B \in (K (D Nat E) R)$
Assertion	fuco22a	$⊢ φ \to B (U P V) A = (x \in {Base}_{C} ⟼ B (1^{st} (M) (x)) (⟨1^{st} (K) (1^{st} (F) (x)), 1^{st} (K) (1^{st} (M) (x))⟩ comp (E) 1^{st} (R) (1^{st} (M) (x))) (1^{st} (F) (x) 2^{nd} (K) 1^{st} (M) (x)) (A (x)))$

Proof

Step	Hyp	Ref	Expression
1		fuco22a.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		fuco22a.u	$⊢ φ \to U = ⟨K, F⟩$
3		fuco22a.v	$⊢ φ \to V = ⟨R, M⟩$
4		fuco22a.a	$⊢ φ \to A \in (F (C Nat D) M)$
5		fuco22a.b	$⊢ φ \to B \in (K (D Nat E) R)$
6		relfunc	$⊢ Rel (D Func E)$
7		df-rel	$⊢ Rel (D Func E) \leftrightarrow D Func E \subseteq V \times V$
8	6 7	mpbi	$⊢ D Func E \subseteq V \times V$
9		eqid	$⊢ D Nat E = D Nat E$
10	9	natrcl	$⊢ B \in (K (D Nat E) R) \to (K \in (D Func E) \land R \in (D Func E))$
11	5 10	syl	$⊢ φ \to (K \in (D Func E) \land R \in (D Func E))$
12	11	simpld	$⊢ φ \to K \in (D Func E)$
13	8 12	sselid	$⊢ φ \to K \in (V \times V)$
14		1st2ndb	$⊢ K \in (V \times V) \leftrightarrow K = ⟨1^{st} (K), 2^{nd} (K)⟩$
15	13 14	sylib	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
16		relfunc	$⊢ Rel (C Func D)$
17		df-rel	$⊢ Rel (C Func D) \leftrightarrow C Func D \subseteq V \times V$
18	16 17	mpbi	$⊢ C Func D \subseteq V \times V$
19		eqid	$⊢ C Nat D = C Nat D$
20	19	natrcl	$⊢ A \in (F (C Nat D) M) \to (F \in (C Func D) \land M \in (C Func D))$
21	4 20	syl	$⊢ φ \to (F \in (C Func D) \land M \in (C Func D))$
22	21	simpld	$⊢ φ \to F \in (C Func D)$
23	18 22	sselid	$⊢ φ \to F \in (V \times V)$
24		1st2ndb	$⊢ F \in (V \times V) \leftrightarrow F = ⟨1^{st} (F), 2^{nd} (F)⟩$
25	23 24	sylib	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
26	15 25	opeq12d	$⊢ φ \to ⟨K, F⟩ = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (F), 2^{nd} (F)⟩⟩$
27	2 26	eqtrd	$⊢ φ \to U = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (F), 2^{nd} (F)⟩⟩$
28	11	simprd	$⊢ φ \to R \in (D Func E)$
29	8 28	sselid	$⊢ φ \to R \in (V \times V)$
30		1st2ndb	$⊢ R \in (V \times V) \leftrightarrow R = ⟨1^{st} (R), 2^{nd} (R)⟩$
31	29 30	sylib	$⊢ φ \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
32	21	simprd	$⊢ φ \to M \in (C Func D)$
33	18 32	sselid	$⊢ φ \to M \in (V \times V)$
34		1st2ndb	$⊢ M \in (V \times V) \leftrightarrow M = ⟨1^{st} (M), 2^{nd} (M)⟩$
35	33 34	sylib	$⊢ φ \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
36	31 35	opeq12d	$⊢ φ \to ⟨R, M⟩ = ⟨⟨1^{st} (R), 2^{nd} (R)⟩, ⟨1^{st} (M), 2^{nd} (M)⟩⟩$
37	3 36	eqtrd	$⊢ φ \to V = ⟨⟨1^{st} (R), 2^{nd} (R)⟩, ⟨1^{st} (M), 2^{nd} (M)⟩⟩$
38	19 4	nat1st2nd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ (C Nat D) ⟨1^{st} (M), 2^{nd} (M)⟩)$
39	9 5	nat1st2nd	$⊢ φ \to B \in (⟨1^{st} (K), 2^{nd} (K)⟩ (D Nat E) ⟨1^{st} (R), 2^{nd} (R)⟩)$
40	1 27 37 38 39	fuco22	$⊢ φ \to B (U P V) A = (x \in {Base}_{C} ⟼ B (1^{st} (M) (x)) (⟨1^{st} (K) (1^{st} (F) (x)), 1^{st} (K) (1^{st} (M) (x))⟩ comp (E) 1^{st} (R) (1^{st} (M) (x))) (1^{st} (F) (x) 2^{nd} (K) 1^{st} (M) (x)) (A (x)))$

Metamath Proof Explorer

Theorem fuco22a

Proof