fuco21

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

	Ref	Expression
Hypotheses	fuco11.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco11.f	$⊢ φ \to F (C Func D) G$
	fuco11.k	$⊢ φ \to K (D Func E) L$
	fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
	fuco21.m	$⊢ φ \to M (C Func D) N$
	fuco21.r	$⊢ φ \to R (D Func E) S$
	fuco21.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
Assertion	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))))$

Proof

Step	Hyp	Ref	Expression
1		fuco11.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		fuco11.f	$⊢ φ \to F (C Func D) G$
3		fuco11.k	$⊢ φ \to K (D Func E) L$
4		fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
5		fuco21.m	$⊢ φ \to M (C Func D) N$
6		fuco21.r	$⊢ φ \to R (D Func E) S$
7		fuco21.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
8	2	funcrcl2	$⊢ φ \to C \in Cat$
9	3	funcrcl2	$⊢ φ \to D \in Cat$
10	3	funcrcl3	$⊢ φ \to E \in Cat$
11		eqidd	$⊢ φ \to (D Func E) \times (C Func D) = (D Func E) \times (C Func D)$
12	8 9 10 1 11	fuco2	$⊢ φ \to P = (u \in ((D Func E) \times (C Func D)), v \in ((D Func E) \times (C Func D)) ⟼ ⦋ 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)))))$
13		fvexd	$⊢ (φ \land (u = U \land v = V)) \to 1^{st} (2^{nd} (u)) \in V$
14		simprl	$⊢ (φ \land (u = U \land v = V)) \to u = U$
15	4	adantr	$⊢ (φ \land (u = U \land v = V)) \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
16	14 15	eqtrd	$⊢ (φ \land (u = U \land v = V)) \to u = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
17	16	fveq2d	$⊢ (φ \land (u = U \land v = V)) \to 2^{nd} (u) = 2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
18	17	fveq2d	$⊢ (φ \land (u = U \land v = V)) \to 1^{st} (2^{nd} (u)) = 1^{st} (2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩))$
19		opex	$⊢ ⟨K, L⟩ \in V$
20		opex	$⊢ ⟨F, G⟩ \in V$
21	19 20	op2nd	$⊢ 2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩) = ⟨F, G⟩$
22	21	fveq2i	$⊢ 1^{st} (2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = 1^{st} (⟨F, G⟩)$
23		relfunc	$⊢ Rel (C Func D)$
24	23	brrelex1i	$⊢ F (C Func D) G \to F \in V$
25	2 24	syl	$⊢ φ \to F \in V$
26	23	brrelex2i	$⊢ F (C Func D) G \to G \in V$
27	2 26	syl	$⊢ φ \to G \in V$
28		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
29	25 27 28	syl2anc	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
30	22 29	eqtrid	$⊢ φ \to 1^{st} (2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = F$
31	30	adantr	$⊢ (φ \land (u = U \land v = V)) \to 1^{st} (2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = F$
32	18 31	eqtrd	$⊢ (φ \land (u = U \land v = V)) \to 1^{st} (2^{nd} (u)) = F$
33		fvexd	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to 1^{st} (1^{st} (u)) \in V$
34	14	adantr	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to u = U$
35	15	adantr	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
36	34 35	eqtrd	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to u = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
37	36	fveq2d	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to 1^{st} (u) = 1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
38	37	fveq2d	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to 1^{st} (1^{st} (u)) = 1^{st} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩))$
39	19 20	op1st	$⊢ 1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩) = ⟨K, L⟩$
40	39	fveq2i	$⊢ 1^{st} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = 1^{st} (⟨K, L⟩)$
41		relfunc	$⊢ Rel (D Func E)$
42	41	brrelex1i	$⊢ K (D Func E) L \to K \in V$
43	3 42	syl	$⊢ φ \to K \in V$
44	41	brrelex2i	$⊢ K (D Func E) L \to L \in V$
45	3 44	syl	$⊢ φ \to L \in V$
46		op1stg	$⊢ (K \in V \land L \in V) \to 1^{st} (⟨K, L⟩) = K$
47	43 45 46	syl2anc	$⊢ φ \to 1^{st} (⟨K, L⟩) = K$
48	40 47	eqtrid	$⊢ φ \to 1^{st} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = K$
49	48	ad2antrr	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to 1^{st} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = K$
50	38 49	eqtrd	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \to 1^{st} (1^{st} (u)) = K$
51		fvexd	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to 2^{nd} (1^{st} (u)) \in V$
52	34	adantr	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to u = U$
53	35	adantr	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
54	52 53	eqtrd	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to u = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
55	54	fveq2d	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to 1^{st} (u) = 1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
56	55	fveq2d	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to 2^{nd} (1^{st} (u)) = 2^{nd} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩))$
57	39	fveq2i	$⊢ 2^{nd} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = 2^{nd} (⟨K, L⟩)$
58		op2ndg	$⊢ (K \in V \land L \in V) \to 2^{nd} (⟨K, L⟩) = L$
59	43 45 58	syl2anc	$⊢ φ \to 2^{nd} (⟨K, L⟩) = L$
60	57 59	eqtrid	$⊢ φ \to 2^{nd} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = L$
61	60	ad3antrrr	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to 2^{nd} (1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)) = L$
62	56 61	eqtrd	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \to 2^{nd} (1^{st} (u)) = L$
63		fvexd	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to 1^{st} (2^{nd} (v)) \in V$
64		simp-4r	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to (u = U \land v = V)$
65	64	simprd	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to v = V$
66	7	ad4antr	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
67	65 66	eqtrd	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to v = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
68	67	fveq2d	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to 2^{nd} (v) = 2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩)$
69	68	fveq2d	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to 1^{st} (2^{nd} (v)) = 1^{st} (2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩))$
70		opex	$⊢ ⟨R, S⟩ \in V$
71		opex	$⊢ ⟨M, N⟩ \in V$
72	70 71	op2nd	$⊢ 2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩) = ⟨M, N⟩$
73	72	fveq2i	$⊢ 1^{st} (2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = 1^{st} (⟨M, N⟩)$
74	23	brrelex1i	$⊢ M (C Func D) N \to M \in V$
75	5 74	syl	$⊢ φ \to M \in V$
76	23	brrelex2i	$⊢ M (C Func D) N \to N \in V$
77	5 76	syl	$⊢ φ \to N \in V$
78		op1stg	$⊢ (M \in V \land N \in V) \to 1^{st} (⟨M, N⟩) = M$
79	75 77 78	syl2anc	$⊢ φ \to 1^{st} (⟨M, N⟩) = M$
80	73 79	eqtrid	$⊢ φ \to 1^{st} (2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = M$
81	80	ad4antr	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to 1^{st} (2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = M$
82	69 81	eqtrd	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \to 1^{st} (2^{nd} (v)) = M$
83		fvexd	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to 1^{st} (1^{st} (v)) \in V$
84	65	adantr	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to v = V$
85	66	adantr	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
86	84 85	eqtrd	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to v = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
87	86	fveq2d	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to 1^{st} (v) = 1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩)$
88	87	fveq2d	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to 1^{st} (1^{st} (v)) = 1^{st} (1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩))$
89	70 71	op1st	$⊢ 1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩) = ⟨R, S⟩$
90	89	fveq2i	$⊢ 1^{st} (1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = 1^{st} (⟨R, S⟩)$
91	41	brrelex1i	$⊢ R (D Func E) S \to R \in V$
92	6 91	syl	$⊢ φ \to R \in V$
93	41	brrelex2i	$⊢ R (D Func E) S \to S \in V$
94	6 93	syl	$⊢ φ \to S \in V$
95		op1stg	$⊢ (R \in V \land S \in V) \to 1^{st} (⟨R, S⟩) = R$
96	92 94 95	syl2anc	$⊢ φ \to 1^{st} (⟨R, S⟩) = R$
97	90 96	eqtrid	$⊢ φ \to 1^{st} (1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = R$
98	97	ad5antr	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to 1^{st} (1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩)) = R$
99	88 98	eqtrd	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \to 1^{st} (1^{st} (v)) = R$
100	55	ad3antrrr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 1^{st} (u) = 1^{st} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
101	100 39	eqtrdi	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 1^{st} (u) = ⟨K, L⟩$
102	87	adantr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 1^{st} (v) = 1^{st} (⟨⟨R, S⟩, ⟨M, N⟩⟩)$
103	102 89	eqtrdi	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 1^{st} (v) = ⟨R, S⟩$
104	101 103	oveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 1^{st} (u) (D Nat E) 1^{st} (v) = ⟨K, L⟩ (D Nat E) ⟨R, S⟩$
105	17	ad5antr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 2^{nd} (u) = 2^{nd} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
106	105 21	eqtrdi	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 2^{nd} (u) = ⟨F, G⟩$
107	68	ad2antrr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 2^{nd} (v) = 2^{nd} (⟨⟨R, S⟩, ⟨M, N⟩⟩)$
108	107 72	eqtrdi	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 2^{nd} (v) = ⟨M, N⟩$
109	106 108	oveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to 2^{nd} (u) (C Nat D) 2^{nd} (v) = ⟨F, G⟩ (C Nat D) ⟨M, N⟩$
110		simp-4r	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to k = K$
111		simp-5r	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to f = F$
112	111	fveq1d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to f (x) = F (x)$
113	110 112	fveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to k (f (x)) = K (F (x))$
114		simplr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to m = M$
115	114	fveq1d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to m (x) = M (x)$
116	110 115	fveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to k (m (x)) = K (M (x))$
117	113 116	opeq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to ⟨k (f (x)), k (m (x))⟩ = ⟨K (F (x)), K (M (x))⟩$
118		simpr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to r = R$
119	118 115	fveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to r (m (x)) = R (M (x))$
120	117 119	oveq12d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to ⟨k (f (x)), k (m (x))⟩ comp (E) r (m (x)) = ⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))$
121	115	fveq2d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to b (m (x)) = b (M (x))$
122		simpllr	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to l = L$
123	122 112 115	oveq123d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to f (x) l m (x) = F (x) L M (x)$
124	123	fveq1d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \to (f (x) l m (x)) (a (x)) = (F (x) L M (x)) (a (x))$
125	120 121 124	oveq123d	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \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))$
126	125	mpteq2dv	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \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)))$
127	104 109 126	mpoeq123dv	$⊢ ((((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \land r = R) \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 (⟨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))))$
128	83 99 127	csbied2	$⊢ (((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \land m = M) \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)))) = (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))))$
129	63 82 128	csbied2	$⊢ ((((φ \land (u = U \land v = V)) \land f = F) \land k = K) \land l = L) \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)))) = (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))))$
130	51 62 129	csbied2	$⊢ (((φ \land (u = U \land v = V)) \land f = F) \land k = K) \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)))) = (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))))$
131	33 50 130	csbied2	$⊢ ((φ \land (u = U \land v = V)) \land f = F) \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)))) = (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))))$
132	13 32 131	csbied2	$⊢ (φ \land (u = U \land v = V)) \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)))) = (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))))$
133	11 4 3 2	fuco2eld	$⊢ φ \to U \in ((D Func E) \times (C Func D))$
134	11 7 6 5	fuco2eld	$⊢ φ \to V \in ((D Func E) \times (C Func D))$
135		ovex	$⊢ ⟨K, L⟩ (D Nat E) ⟨R, S⟩ \in V$
136		ovex	$⊢ ⟨F, G⟩ (C Nat D) ⟨M, N⟩ \in V$
137	135 136	mpoex	$⊢ (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)))) \in V$
138	137	a1i	$⊢ φ \to (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)))) \in V$
139	12 132 133 134 138	ovmpod	$⊢ φ \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))))$

Metamath Proof Explorer

Theorem fuco21

Proof