fucofvalg

Description: Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	fucofvalg.p	$⊢ φ \to P \in U$
	fucofvalg.c	$⊢ φ \to 1^{st} (P) = C$
	fucofvalg.d	$⊢ φ \to 2^{nd} (P) = D$
	fucofvalg.e	$⊢ φ \to E \in V$
	fucofvalg.o	No typesetting found for \|- ( ph -> ( P o.F E ) = .o. ) with typecode \|-
	fucofvalg.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
Assertion	fucofvalg	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		fucofvalg.p	$⊢ φ \to P \in U$
2		fucofvalg.c	$⊢ φ \to 1^{st} (P) = C$
3		fucofvalg.d	$⊢ φ \to 2^{nd} (P) = D$
4		fucofvalg.e	$⊢ φ \to E \in V$
5		fucofvalg.o	Could not format ( ph -> ( P o.F E ) = .o. ) : No typesetting found for \|- ( ph -> ( P o.F E ) = .o. ) with typecode \|-
6		fucofvalg.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
7		df-fuco	Could not format o.F = ( p e. _V , e e. _V \|-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( 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 \|- o.F = ( p e. _V , e e. _V \|-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( 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 \|-
8	7	a1i	Could not format ( ph -> o.F = ( p e. _V , e e. _V \|-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( 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.F = ( p e. _V , e e. _V \|-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( 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 \|-
9		fvexd	$⊢ (φ \land (p = P \land e = E)) \to 1^{st} (p) \in V$
10		simprl	$⊢ (φ \land (p = P \land e = E)) \to p = P$
11	10	fveq2d	$⊢ (φ \land (p = P \land e = E)) \to 1^{st} (p) = 1^{st} (P)$
12	2	adantr	$⊢ (φ \land (p = P \land e = E)) \to 1^{st} (P) = C$
13	11 12	eqtrd	$⊢ (φ \land (p = P \land e = E)) \to 1^{st} (p) = C$
14		fvexd	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to 2^{nd} (p) \in V$
15		simplrl	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to p = P$
16	15	fveq2d	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to 2^{nd} (p) = 2^{nd} (P)$
17	3	ad2antrr	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to 2^{nd} (P) = D$
18	16 17	eqtrd	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to 2^{nd} (p) = D$
19		simpr	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to d = D$
20		simpllr	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to (p = P \land e = E)$
21	20	simprd	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to e = E$
22	19 21	oveq12d	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to d Func e = D Func E$
23		simplr	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to c = C$
24	23 19	oveq12d	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to c Func d = C Func D$
25	22 24	xpeq12d	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to (d Func e) \times (c Func d) = (D Func E) \times (C Func D)$
26		ovexd	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to D Func E \in V$
27		ovexd	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to C Func D \in V$
28	26 27	xpexd	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to (D Func E) \times (C Func D) \in V$
29	25 28	eqeltrd	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to (d Func e) \times (c Func d) \in V$
30	6	ad3antrrr	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to W = (D Func E) \times (C Func D)$
31	25 30	eqtr4d	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to (d Func e) \times (c Func d) = W$
32		simpr	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to w = W$
33	32	reseq2d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to {\circ_{func} ↾}_{w} = {\circ_{func} ↾}_{W}$
34		simplr	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to d = D$
35	21	adantr	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to e = E$
36	34 35	oveq12d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to d Nat e = D Nat E$
37	36	oveqd	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to 1^{st} (u) (d Nat e) 1^{st} (v) = 1^{st} (u) (D Nat E) 1^{st} (v)$
38		simpllr	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to c = C$
39	38 34	oveq12d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to c Nat d = C Nat D$
40	39	oveqd	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to 2^{nd} (u) (c Nat d) 2^{nd} (v) = 2^{nd} (u) (C Nat D) 2^{nd} (v)$
41	38	fveq2d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to {Base}_{c} = {Base}_{C}$
42	35	fveq2d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to comp (e) = comp (E)$
43	42	oveqd	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⟨k (f (x)), k (m (x))⟩ comp (e) r (m (x)) = ⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x))$
44	43	oveqd	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \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))$
45	41 44	mpteq12dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \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)))$
46	37 40 45	mpoeq123dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to (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)))) = (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))))$
47	46	csbeq2dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⦋ 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)))) = ⦋ 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))))$
48	47	csbeq2dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⦋ 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)))) = ⦋ 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))))$
49	48	csbeq2dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⦋ 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)))) = ⦋ 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))))$
50	49	csbeq2dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⦋ 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)))) = ⦋ 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))))$
51	50	csbeq2dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⦋ 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)))) = ⦋ 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))))$
52	32 32 51	mpoeq123dv	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to (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))))) = (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)))))$
53	33 52	opeq12d	$⊢ ((((φ \land (p = P \land e = E)) \land c = C) \land d = D) \land w = W) \to ⟨{\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)))))⟩ = ⟨{\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)))))⟩$
54	29 31 53	csbied2	$⊢ (((φ \land (p = P \land e = E)) \land c = C) \land d = D) \to ⦋ ((d Func e) \times (c Func d)) / w ⦌ ⟨{\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)))))⟩ = ⟨{\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)))))⟩$
55	14 18 54	csbied2	$⊢ ((φ \land (p = P \land e = E)) \land c = C) \to ⦋ 2^{nd} (p) / d ⦌ ⦋ ((d Func e) \times (c Func d)) / w ⦌ ⟨{\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)))))⟩ = ⟨{\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)))))⟩$
56	9 13 55	csbied2	$⊢ (φ \land (p = P \land e = E)) \to ⦋ 1^{st} (p) / c ⦌ ⦋ 2^{nd} (p) / d ⦌ ⦋ ((d Func e) \times (c Func d)) / w ⦌ ⟨{\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)))))⟩ = ⟨{\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)))))⟩$
57	1	elexd	$⊢ φ \to P \in V$
58	4	elexd	$⊢ φ \to E \in V$
59		opex	$⊢ ⟨{\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)))))⟩ \in V$
60	59	a1i	$⊢ φ \to ⟨{\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)))))⟩ \in V$
61	8 56 57 58 60	ovmpod	Could not format ( ph -> ( P o.F E ) = <. ( 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 -> ( P o.F E ) = <. ( 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 \|-
62	5 61	eqtr3d	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 fucofvalg

Proof