fucofvalne

Description: Value of the function giving the functor composition bifunctor, if C or D are not sets. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	fucofvalne.c	$⊢ φ \to \neg (C \in V \land D \in V)$
	fucofvalne.e	$⊢ φ \to E \in Cat$
	fucofvalne.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode \|-
	fucofvalne.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
Assertion	fucofvalne	Could not format assertion : No typesetting found for \|- ( ph -> .o. =/= <. ( o.func \|` W ) , ( u e. W , v e. W \|-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) \|-> ( x e. ( Base ` C ) \|-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		fucofvalne.c	$⊢ φ \to \neg (C \in V \land D \in V)$
2		fucofvalne.e	$⊢ φ \to E \in Cat$
3		fucofvalne.o	Could not format ( ph -> ( <. C , D >. o.F E ) = .o. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode \|-
4		fucofvalne.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
5		0ex	$⊢ \emptyset \in V$
6	5	a1i	$⊢ φ \to \emptyset \in V$
7		1st0	$⊢ 1^{st} (\emptyset) = \emptyset$
8	7	a1i	$⊢ φ \to 1^{st} (\emptyset) = \emptyset$
9		2nd0	$⊢ 2^{nd} (\emptyset) = \emptyset$
10	9	a1i	$⊢ φ \to 2^{nd} (\emptyset) = \emptyset$
11		opprc	$⊢ \neg (C \in V \land D \in V) \to ⟨C, D⟩ = \emptyset$
12	1 11	syl	$⊢ φ \to ⟨C, D⟩ = \emptyset$
13	12	oveq1d	Could not format ( ph -> ( <. C , D >. o.F E ) = ( (/) o.F E ) ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = ( (/) o.F E ) ) with typecode \|-
14	13 3	eqtr3d	Could not format ( ph -> ( (/) o.F E ) = .o. ) : No typesetting found for \|- ( ph -> ( (/) o.F E ) = .o. ) with typecode \|-
15		eqidd	$⊢ φ \to (\emptyset Func E) \times (\emptyset Func \emptyset) = (\emptyset Func E) \times (\emptyset Func \emptyset)$
16	6 8 10 2 14 15	fucofvalg	Could not format ( ph -> .o. = <. ( o.func \|` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) \|-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) \|-> ( x e. ( Base ` (/) ) \|-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) : No typesetting found for \|- ( ph -> .o. = <. ( o.func \|` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) \|-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) \|-> ( x e. ( Base ` (/) ) \|-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode \|-
17		opex	$⊢ ⟨\emptyset, \emptyset⟩ \in V$
18	17	snnz	$⊢ \{⟨\emptyset, \emptyset⟩\} \neq \emptyset$
19	18	neii	$⊢ \neg \{⟨\emptyset, \emptyset⟩\} = \emptyset$
20		ioran	$⊢ \neg (\{⟨\emptyset, \emptyset⟩\} = \emptyset \lor \{⟨\emptyset, \emptyset⟩\} = \emptyset) \leftrightarrow (\neg \{⟨\emptyset, \emptyset⟩\} = \emptyset \land \neg \{⟨\emptyset, \emptyset⟩\} = \emptyset)$
21		xpeq0	$⊢ \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset \leftrightarrow (\{⟨\emptyset, \emptyset⟩\} = \emptyset \lor \{⟨\emptyset, \emptyset⟩\} = \emptyset)$
22	21	biimpi	$⊢ \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset \to (\{⟨\emptyset, \emptyset⟩\} = \emptyset \lor \{⟨\emptyset, \emptyset⟩\} = \emptyset)$
23	22	con3i	$⊢ \neg (\{⟨\emptyset, \emptyset⟩\} = \emptyset \lor \{⟨\emptyset, \emptyset⟩\} = \emptyset) \to \neg \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset$
24	20 23	sylbir	$⊢ (\neg \{⟨\emptyset, \emptyset⟩\} = \emptyset \land \neg \{⟨\emptyset, \emptyset⟩\} = \emptyset) \to \neg \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset$
25	19 19 24	mp2an	$⊢ \neg \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset$
26	2	0func	$⊢ φ \to \emptyset Func E = \{⟨\emptyset, \emptyset⟩\}$
27		0cat	$⊢ \emptyset \in Cat$
28	27	a1i	$⊢ φ \to \emptyset \in Cat$
29	28	0func	$⊢ φ \to \emptyset Func \emptyset = \{⟨\emptyset, \emptyset⟩\}$
30	26 29	xpeq12d	$⊢ φ \to (\emptyset Func E) \times (\emptyset Func \emptyset) = \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\}$
31		df-func	$⊢ Func = (t \in Cat, u \in Cat ⟼ \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))\})$
32	31	reldmmpo	$⊢ Rel dom Func$
33		0nelrel0	$⊢ Rel dom Func \to \neg \emptyset \in dom Func$
34	32 33	ax-mp	$⊢ \neg \emptyset \in dom Func$
35	12	eleq1d	$⊢ φ \to (⟨C, D⟩ \in dom Func \leftrightarrow \emptyset \in dom Func)$
36	34 35	mtbiri	$⊢ φ \to \neg ⟨C, D⟩ \in dom Func$
37		df-ov	$⊢ C Func D = Func (⟨C, D⟩)$
38		ndmfv	$⊢ \neg ⟨C, D⟩ \in dom Func \to Func (⟨C, D⟩) = \emptyset$
39	37 38	eqtrid	$⊢ \neg ⟨C, D⟩ \in dom Func \to C Func D = \emptyset$
40	39	xpeq2d	$⊢ \neg ⟨C, D⟩ \in dom Func \to (D Func E) \times (C Func D) = (D Func E) \times \emptyset$
41		xp0	$⊢ (D Func E) \times \emptyset = \emptyset$
42	40 41	eqtrdi	$⊢ \neg ⟨C, D⟩ \in dom Func \to (D Func E) \times (C Func D) = \emptyset$
43	36 42	syl	$⊢ φ \to (D Func E) \times (C Func D) = \emptyset$
44	30 43	eqeq12d	$⊢ φ \to ((\emptyset Func E) \times (\emptyset Func \emptyset) = (D Func E) \times (C Func D) \leftrightarrow \{⟨\emptyset, \emptyset⟩\} \times \{⟨\emptyset, \emptyset⟩\} = \emptyset)$
45	25 44	mtbiri	$⊢ φ \to \neg (\emptyset Func E) \times (\emptyset Func \emptyset) = (D Func E) \times (C Func D)$
46		rescofuf	$⊢ ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) : (\emptyset Func E) \times (\emptyset Func \emptyset) ⟶ \emptyset Func E$
47	46	fdmi	$⊢ dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = (\emptyset Func E) \times (\emptyset Func \emptyset)$
48		rescofuf	$⊢ ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$
49	48	fdmi	$⊢ dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) = (D Func E) \times (C Func D)$
50	47 49	eqeq12i	$⊢ dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) \leftrightarrow (\emptyset Func E) \times (\emptyset Func \emptyset) = (D Func E) \times (C Func D)$
51	50	biimpi	$⊢ dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) \to (\emptyset Func E) \times (\emptyset Func \emptyset) = (D Func E) \times (C Func D)$
52	51	con3i	$⊢ \neg (\emptyset Func E) \times (\emptyset Func \emptyset) = (D Func E) \times (C Func D) \to \neg dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))})$
53		dmeq	$⊢ {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))} \to dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))})$
54	53	con3i	$⊢ \neg dom ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) = dom ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) \to \neg {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
55	45 52 54	3syl	$⊢ φ \to \neg {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
56	55	neqned	$⊢ φ \to {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \neq {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
57	4	reseq2d	$⊢ φ \to {\circ_{func} ↾}_{W} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
58	56 57	neeqtrrd	$⊢ φ \to {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \neq {\circ_{func} ↾}_{W}$
59		ovex	$⊢ \emptyset Func E \in V$
60		ovex	$⊢ \emptyset Func \emptyset \in V$
61	59 60	xpex	$⊢ (\emptyset Func E) \times (\emptyset Func \emptyset) \in V$
62		fex	$⊢ (({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}) : (\emptyset Func E) \times (\emptyset Func \emptyset) ⟶ \emptyset Func E \land (\emptyset Func E) \times (\emptyset Func \emptyset) \in V) \to {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \in V$
63	46 61 62	mp2an	$⊢ {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \in V$
64	61 61	mpoex	$⊢ (u \in ((\emptyset Func E) \times (\emptyset Func \emptyset)), v \in ((\emptyset Func E) \times (\emptyset Func \emptyset)) ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (\emptyset Nat E) 1^{st} (v)), a \in (2^{nd} (u) (\emptyset Nat \emptyset) 2^{nd} (v)) ⟼ (x \in {Base}_{\emptyset} ⟼ b (m (x)) (⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))) (f (x) l m (x)) (a (x))))) \in V$
65		opth1neg	$⊢ ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \in V \land (u \in ((\emptyset Func E) \times (\emptyset Func \emptyset)), v \in ((\emptyset Func E) \times (\emptyset Func \emptyset)) ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (\emptyset Nat E) 1^{st} (v)), a \in (2^{nd} (u) (\emptyset Nat \emptyset) 2^{nd} (v)) ⟼ (x \in {Base}_{\emptyset} ⟼ b (m (x)) (⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))) (f (x) l m (x)) (a (x))))) \in V) \to ({\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \neq {\circ_{func} ↾}_{W} \to ⟨{\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}, (u \in ((\emptyset Func E) \times (\emptyset Func \emptyset)), v \in ((\emptyset Func E) \times (\emptyset Func \emptyset)) ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (\emptyset Nat E) 1^{st} (v)), a \in (2^{nd} (u) (\emptyset Nat \emptyset) 2^{nd} (v)) ⟼ (x \in {Base}_{\emptyset} ⟼ b (m (x)) (⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))) (f (x) l m (x)) (a (x)))))⟩ \neq ⟨{\circ_{func} ↾}_{W}, (u \in W, v \in W ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (D Nat E) 1^{st} (v)), a \in (2^{nd} (u) (C Nat D) 2^{nd} (v)) ⟼ (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)))))⟩)$
66	63 64 65	mp2an	$⊢ {\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))} \neq {\circ_{func} ↾}_{W} \to ⟨{\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}, (u \in ((\emptyset Func E) \times (\emptyset Func \emptyset)), v \in ((\emptyset Func E) \times (\emptyset Func \emptyset)) ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (\emptyset Nat E) 1^{st} (v)), a \in (2^{nd} (u) (\emptyset Nat \emptyset) 2^{nd} (v)) ⟼ (x \in {Base}_{\emptyset} ⟼ b (m (x)) (⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))) (f (x) l m (x)) (a (x)))))⟩ \neq ⟨{\circ_{func} ↾}_{W}, (u \in W, v \in W ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (D Nat E) 1^{st} (v)), a \in (2^{nd} (u) (C Nat D) 2^{nd} (v)) ⟼ (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)))))⟩$
67	58 66	syl	$⊢ φ \to ⟨{\circ_{func} ↾}_{((\emptyset Func E) \times (\emptyset Func \emptyset))}, (u \in ((\emptyset Func E) \times (\emptyset Func \emptyset)), v \in ((\emptyset Func E) \times (\emptyset Func \emptyset)) ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (\emptyset Nat E) 1^{st} (v)), a \in (2^{nd} (u) (\emptyset Nat \emptyset) 2^{nd} (v)) ⟼ (x \in {Base}_{\emptyset} ⟼ b (m (x)) (⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))) (f (x) l m (x)) (a (x)))))⟩ \neq ⟨{\circ_{func} ↾}_{W}, (u \in W, v \in W ⟼ ⦋ 1^{st} (2^{nd} (u)) / f ⦌ ⦋ 1^{st} (1^{st} (u)) / k ⦌ ⦋ 2^{nd} (1^{st} (u)) / l ⦌ ⦋ 1^{st} (2^{nd} (v)) / m ⦌ ⦋ 1^{st} (1^{st} (v)) / r ⦌ (b \in (1^{st} (u) (D Nat E) 1^{st} (v)), a \in (2^{nd} (u) (C Nat D) 2^{nd} (v)) ⟼ (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)))))⟩$
68	16 67	eqnetrd	Could not format ( ph -> .o. =/= <. ( o.func \|` W ) , ( u e. W , v e. W \|-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) \|-> ( x e. ( Base ` C ) \|-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) : No typesetting found for \|- ( ph -> .o. =/= <. ( o.func \|` W ) , ( u e. W , v e. W \|-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) \|-> ( x e. ( Base ` C ) \|-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode \|-

Metamath Proof Explorer

Theorem fucofvalne

Proof