fuco22

Description: The morphism part of the functor composition bifunctor. See also fuco22a . (Contributed by Zhi Wang, 29-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fuco22.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		fuco22.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
3		fuco22.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
4		fuco22.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
5		fuco22.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
6		eqid	$⊢ C Nat D = C Nat D$
7	6 4	natrcl2	$⊢ φ \to F (C Func D) G$
8		eqid	$⊢ D Nat E = D Nat E$
9	8 5	natrcl2	$⊢ φ \to K (D Func E) L$
10	6 4	natrcl3	$⊢ φ \to M (C Func D) N$
11	8 5	natrcl3	$⊢ φ \to R (D Func E) S$
12	1 7 9 2 10 11 3	fuco21	$⊢ φ \to U P V = (b \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩), a \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩) ⟼ (x \in {Base}_{C} ⟼ b (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (a (x))))$
13		simplrl	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to b = B$
14	13	fveq1d	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to b (M (x)) = B (M (x))$
15		simplrr	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to a = A$
16	15	fveq1d	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to a (x) = A (x)$
17	16	fveq2d	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to (F (x) L M (x)) (a (x)) = (F (x) L M (x)) (A (x))$
18	14 17	oveq12d	$⊢ ((φ \land (b = B \land a = A)) \land x \in {Base}_{C}) \to b (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (a (x)) = B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x))$
19	18	mpteq2dva	$⊢ (φ \land (b = B \land a = A)) \to (x \in {Base}_{C} ⟼ b (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (a (x))) = (x \in {Base}_{C} ⟼ B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)))$
20		fvexd	$⊢ φ \to {Base}_{C} \in V$
21	20	mptexd	$⊢ φ \to (x \in {Base}_{C} ⟼ B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x))) \in V$
22	12 19 5 4 21	ovmpod	$⊢ φ \to B (U P V) A = (x \in {Base}_{C} ⟼ B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)))$

Metamath Proof Explorer

Theorem fuco22

Proof