Metamath Proof Explorer

Theorem fucofn22

Description: The morphism part of the functor composition bifunctor maps two natural transformations to a function on a base set. (Contributed by Zhi Wang, 30-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	fucofn22	$⊢ φ \to (B (U P V) A) Fn {Base}_{C}$

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		ovex	$⊢ B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)) \in V$
7		eqid	$⊢ (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)))$
8	6 7	fnmpti	$⊢ (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))) Fn {Base}_{C}$
9	1 2 3 4 5	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)))$
10	9	fneq1d	$⊢ φ \to ((B (U P V) A) Fn {Base}_{C} \leftrightarrow (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))) Fn {Base}_{C})$
11	8 10	mpbiri	$⊢ φ \to (B (U P V) A) Fn {Base}_{C}$