evlfcl

Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors C --> D , and the second parameter in D . (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	evlfcl.e	$⊢ E = C {eval}_{F} D$
	evlfcl.q	$⊢ Q = C FuncCat D$
	evlfcl.c	$⊢ φ \to C \in Cat$
	evlfcl.d	$⊢ φ \to D \in Cat$
Assertion	evlfcl	$⊢ φ \to E \in ((Q \times_{c} C) Func D)$

Proof

Step	Hyp	Ref	Expression
1		evlfcl.e	$⊢ E = C {eval}_{F} D$
2		evlfcl.q	$⊢ Q = C FuncCat D$
3		evlfcl.c	$⊢ φ \to C \in Cat$
4		evlfcl.d	$⊢ φ \to D \in Cat$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		eqid	$⊢ Hom (C) = Hom (C)$
7		eqid	$⊢ comp (D) = comp (D)$
8		eqid	$⊢ C Nat D = C Nat D$
9	1 3 4 5 6 7 8	evlfval	$⊢ φ \to E = ⟨(f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$
10		ovex	$⊢ C Func D \in V$
11		fvex	$⊢ {Base}_{C} \in V$
12	10 11	mpoex	$⊢ (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)) \in V$
13	10 11	xpex	$⊢ (C Func D) \times {Base}_{C} \in V$
14	13 13	mpoex	$⊢ (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) \in V$
15	12 14	opelvv	$⊢ ⟨(f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \in (V \times V)$
16	9 15	eqeltrdi	$⊢ φ \to E \in (V \times V)$
17		1st2nd2	$⊢ E \in (V \times V) \to E = ⟨1^{st} (E), 2^{nd} (E)⟩$
18	16 17	syl	$⊢ φ \to E = ⟨1^{st} (E), 2^{nd} (E)⟩$
19		eqid	$⊢ Q \times_{c} C = Q \times_{c} C$
20	2	fucbas	$⊢ C Func D = {Base}_{Q}$
21	19 20 5	xpcbas	$⊢ (C Func D) \times {Base}_{C} = {Base}_{(Q \times_{c} C)}$
22		eqid	$⊢ {Base}_{D} = {Base}_{D}$
23		eqid	$⊢ Hom (Q \times_{c} C) = Hom (Q \times_{c} C)$
24		eqid	$⊢ Hom (D) = Hom (D)$
25		eqid	$⊢ Id (Q \times_{c} C) = Id (Q \times_{c} C)$
26		eqid	$⊢ Id (D) = Id (D)$
27		eqid	$⊢ comp (Q \times_{c} C) = comp (Q \times_{c} C)$
28	2 3 4	fuccat	$⊢ φ \to Q \in Cat$
29	19 28 3	xpccat	$⊢ φ \to Q \times_{c} C \in Cat$
30		relfunc	$⊢ Rel (C Func D)$
31		simpr	$⊢ (φ \land f \in (C Func D)) \to f \in (C Func D)$
32		1st2ndbr	$⊢ (Rel (C Func D) \land f \in (C Func D)) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
33	30 31 32	sylancr	$⊢ (φ \land f \in (C Func D)) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
34	5 22 33	funcf1	$⊢ (φ \land f \in (C Func D)) \to 1^{st} (f) : {Base}_{C} ⟶ {Base}_{D}$
35	34	ffvelrnda	$⊢ ((φ \land f \in (C Func D)) \land x \in {Base}_{C}) \to 1^{st} (f) (x) \in {Base}_{D}$
36	35	ralrimiva	$⊢ (φ \land f \in (C Func D)) \to \forall x \in {Base}_{C} 1^{st} (f) (x) \in {Base}_{D}$
37	36	ralrimiva	$⊢ φ \to \forall f \in (C Func D) \forall x \in {Base}_{C} 1^{st} (f) (x) \in {Base}_{D}$
38		eqid	$⊢ (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)) = (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x))$
39	38	fmpo	$⊢ \forall f \in (C Func D) \forall x \in {Base}_{C} 1^{st} (f) (x) \in {Base}_{D} \leftrightarrow (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)) : (C Func D) \times {Base}_{C} ⟶ {Base}_{D}$
40	37 39	sylib	$⊢ φ \to (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)) : (C Func D) \times {Base}_{C} ⟶ {Base}_{D}$
41	12 14	op1std	$⊢ E = ⟨(f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \to 1^{st} (E) = (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x))$
42	9 41	syl	$⊢ φ \to 1^{st} (E) = (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x))$
43	42	feq1d	$⊢ φ \to (1^{st} (E) : (C Func D) \times {Base}_{C} ⟶ {Base}_{D} \leftrightarrow (f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)) : (C Func D) \times {Base}_{C} ⟶ {Base}_{D})$
44	40 43	mpbird	$⊢ φ \to 1^{st} (E) : (C Func D) \times {Base}_{C} ⟶ {Base}_{D}$
45		eqid	$⊢ (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) = (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))$
46		ovex	$⊢ m (C Nat D) n \in V$
47		ovex	$⊢ 2^{nd} (x) Hom (C) 2^{nd} (y) \in V$
48	46 47	mpoex	$⊢ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) \in V$
49	48	csbex	$⊢ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) \in V$
50	49	csbex	$⊢ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) \in V$
51	45 50	fnmpoi	$⊢ (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) Fn (((C Func D) \times {Base}_{C}) \times ((C Func D) \times {Base}_{C}))$
52	12 14	op2ndd	$⊢ E = ⟨(f \in (C Func D), x \in {Base}_{C} ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \to 2^{nd} (E) = (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))$
53	9 52	syl	$⊢ φ \to 2^{nd} (E) = (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))$
54	53	fneq1d	$⊢ φ \to (2^{nd} (E) Fn (((C Func D) \times {Base}_{C}) \times ((C Func D) \times {Base}_{C})) \leftrightarrow (x \in ((C Func D) \times {Base}_{C}), y \in ((C Func D) \times {Base}_{C}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) Fn (((C Func D) \times {Base}_{C}) \times ((C Func D) \times {Base}_{C})))$
55	51 54	mpbiri	$⊢ φ \to 2^{nd} (E) Fn (((C Func D) \times {Base}_{C}) \times ((C Func D) \times {Base}_{C}))$
56	4	ad2antrr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to D \in Cat$
57	56	adantr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to D \in Cat$
58		simplrl	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to f \in (C Func D)$
59	30 58 32	sylancr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
60	5 22 59	funcf1	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to 1^{st} (f) : {Base}_{C} ⟶ {Base}_{D}$
61	60	adantr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to 1^{st} (f) : {Base}_{C} ⟶ {Base}_{D}$
62		simplrr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to u \in {Base}_{C}$
63	62	adantr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to u \in {Base}_{C}$
64	61 63	ffvelrnd	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to 1^{st} (f) (u) \in {Base}_{D}$
65		simplrr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to v \in {Base}_{C}$
66	61 65	ffvelrnd	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to 1^{st} (f) (v) \in {Base}_{D}$
67		simprl	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to g \in (C Func D)$
68		1st2ndbr	$⊢ (Rel (C Func D) \land g \in (C Func D)) \to 1^{st} (g) (C Func D) 2^{nd} (g)$
69	30 67 68	sylancr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to 1^{st} (g) (C Func D) 2^{nd} (g)$
70	5 22 69	funcf1	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to 1^{st} (g) : {Base}_{C} ⟶ {Base}_{D}$
71	70	adantr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to 1^{st} (g) : {Base}_{C} ⟶ {Base}_{D}$
72	71 65	ffvelrnd	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to 1^{st} (g) (v) \in {Base}_{D}$
73		simprr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to v \in {Base}_{C}$
74	5 6 24 59 62 73	funcf2	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to (u 2^{nd} (f) v) : u Hom (C) v ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (f) (v)$
75	74	adantr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to (u 2^{nd} (f) v) : u Hom (C) v ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (f) (v)$
76		simprr	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to h \in (u Hom (C) v)$
77	75 76	ffvelrnd	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to (u 2^{nd} (f) v) (h) \in (1^{st} (f) (u) Hom (D) 1^{st} (f) (v))$
78		simprl	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to a \in (f (C Nat D) g)$
79	8 78	nat1st2nd	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to a \in (⟨1^{st} (f), 2^{nd} (f)⟩ (C Nat D) ⟨1^{st} (g), 2^{nd} (g)⟩)$
80	8 79 5 24 65	natcl	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to a (v) \in (1^{st} (f) (v) Hom (D) 1^{st} (g) (v))$
81	22 24 7 57 64 66 72 77 80	catcocl	$⊢ (((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \land (a \in (f (C Nat D) g) \land h \in (u Hom (C) v))) \to a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h) \in (1^{st} (f) (u) Hom (D) 1^{st} (g) (v))$
82	81	ralrimivva	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to \forall a \in (f (C Nat D) g) \forall h \in (u Hom (C) v) a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h) \in (1^{st} (f) (u) Hom (D) 1^{st} (g) (v))$
83		eqid	$⊢ (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h)) = (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h))$
84	83	fmpo	$⊢ \forall a \in (f (C Nat D) g) \forall h \in (u Hom (C) v) a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h) \in (1^{st} (f) (u) Hom (D) 1^{st} (g) (v)) \leftrightarrow (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h)) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v)$
85	82 84	sylib	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h)) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v)$
86	3	ad2antrr	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to C \in Cat$
87		eqid	$⊢ ⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩ = ⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩$
88	1 86 56 5 6 7 8 58 67 62 73 87	evlf2	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to ⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩ = (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h))$
89	88	feq1d	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to ((⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v) \leftrightarrow (a \in (f (C Nat D) g), h \in (u Hom (C) v) ⟼ a (v) (⟨1^{st} (f) (u), 1^{st} (f) (v)⟩ comp (D) 1^{st} (g) (v)) (u 2^{nd} (f) v) (h)) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v))$
90	85 89	mpbird	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v)$
91	2 8	fuchom	$⊢ C Nat D = Hom (Q)$
92	19 20 5 91 6 58 62 67 73 23	xpchom2	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ = (f (C Nat D) g) \times (u Hom (C) v)$
93	1 86 56 5 58 62	evlf1	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to f 1^{st} (E) u = 1^{st} (f) (u)$
94	1 86 56 5 67 73	evlf1	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to g 1^{st} (E) v = 1^{st} (g) (v)$
95	93 94	oveq12d	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v) = 1^{st} (f) (u) Hom (D) 1^{st} (g) (v)$
96	92 95	feq23d	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to ((⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v) \leftrightarrow (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : (f (C Nat D) g) \times (u Hom (C) v) ⟶ 1^{st} (f) (u) Hom (D) 1^{st} (g) (v))$
97	90 96	mpbird	$⊢ ((φ \land (f \in (C Func D) \land u \in {Base}_{C})) \land (g \in (C Func D) \land v \in {Base}_{C})) \to (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v)$
98	97	ralrimivva	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to \forall g \in (C Func D) \forall v \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v)$
99	98	ralrimivva	$⊢ φ \to \forall f \in (C Func D) \forall u \in {Base}_{C} \forall g \in (C Func D) \forall v \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v)$
100		oveq2	$⊢ y = ⟨g, v⟩ \to x 2^{nd} (E) y = x 2^{nd} (E) ⟨g, v⟩$
101		oveq2	$⊢ y = ⟨g, v⟩ \to x Hom (Q \times_{c} C) y = x Hom (Q \times_{c} C) ⟨g, v⟩$
102		fveq2	$⊢ y = ⟨g, v⟩ \to 1^{st} (E) (y) = 1^{st} (E) (⟨g, v⟩)$
103		df-ov	$⊢ g 1^{st} (E) v = 1^{st} (E) (⟨g, v⟩)$
104	102 103	eqtr4di	$⊢ y = ⟨g, v⟩ \to 1^{st} (E) (y) = g 1^{st} (E) v$
105	104	oveq2d	$⊢ y = ⟨g, v⟩ \to 1^{st} (E) (x) Hom (D) 1^{st} (E) (y) = 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v)$
106	100 101 105	feq123d	$⊢ y = ⟨g, v⟩ \to ((x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y) \leftrightarrow (x 2^{nd} (E) ⟨g, v⟩) : x Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v))$
107	106	ralxp	$⊢ \forall y \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y) \leftrightarrow \forall g \in (C Func D) \forall v \in {Base}_{C} (x 2^{nd} (E) ⟨g, v⟩) : x Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v)$
108		oveq1	$⊢ x = ⟨f, u⟩ \to x 2^{nd} (E) ⟨g, v⟩ = ⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩$
109		oveq1	$⊢ x = ⟨f, u⟩ \to x Hom (Q \times_{c} C) ⟨g, v⟩ = ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩$
110		fveq2	$⊢ x = ⟨f, u⟩ \to 1^{st} (E) (x) = 1^{st} (E) (⟨f, u⟩)$
111		df-ov	$⊢ f 1^{st} (E) u = 1^{st} (E) (⟨f, u⟩)$
112	110 111	eqtr4di	$⊢ x = ⟨f, u⟩ \to 1^{st} (E) (x) = f 1^{st} (E) u$
113	112	oveq1d	$⊢ x = ⟨f, u⟩ \to 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v) = (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v)$
114	108 109 113	feq123d	$⊢ x = ⟨f, u⟩ \to ((x 2^{nd} (E) ⟨g, v⟩) : x Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v) \leftrightarrow (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v))$
115	114	2ralbidv	$⊢ x = ⟨f, u⟩ \to (\forall g \in (C Func D) \forall v \in {Base}_{C} (x 2^{nd} (E) ⟨g, v⟩) : x Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ 1^{st} (E) (x) Hom (D) (g 1^{st} (E) v) \leftrightarrow \forall g \in (C Func D) \forall v \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v))$
116	107 115	syl5bb	$⊢ x = ⟨f, u⟩ \to (\forall y \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y) \leftrightarrow \forall g \in (C Func D) \forall v \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v))$
117	116	ralxp	$⊢ \forall x \in ((C Func D) \times {Base}_{C}) \forall y \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y) \leftrightarrow \forall f \in (C Func D) \forall u \in {Base}_{C} \forall g \in (C Func D) \forall v \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨g, v⟩) : ⟨f, u⟩ Hom (Q \times_{c} C) ⟨g, v⟩ ⟶ (f 1^{st} (E) u) Hom (D) (g 1^{st} (E) v)$
118	99 117	sylibr	$⊢ φ \to \forall x \in ((C Func D) \times {Base}_{C}) \forall y \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y)$
119	118	r19.21bi	$⊢ (φ \land x \in ((C Func D) \times {Base}_{C})) \to \forall y \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y)$
120	119	r19.21bi	$⊢ ((φ \land x \in ((C Func D) \times {Base}_{C})) \land y \in ((C Func D) \times {Base}_{C})) \to (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y)$
121	120	anasss	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}))) \to (x 2^{nd} (E) y) : x Hom (Q \times_{c} C) y ⟶ 1^{st} (E) (x) Hom (D) 1^{st} (E) (y)$
122	28	adantr	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Q \in Cat$
123	3	adantr	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to C \in Cat$
124		eqid	$⊢ Id (Q) = Id (Q)$
125		eqid	$⊢ Id (C) = Id (C)$
126		simprl	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to f \in (C Func D)$
127		simprr	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to u \in {Base}_{C}$
128	19 122 123 20 5 124 125 25 126 127	xpcid	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q \times_{c} C) (⟨f, u⟩) = ⟨Id (Q) (f), Id (C) (u)⟩$
129	128	fveq2d	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (⟨Id (Q) (f), Id (C) (u)⟩)$
130		df-ov	$⊢ Id (Q) (f) (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) Id (C) (u) = (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (⟨Id (Q) (f), Id (C) (u)⟩)$
131	129 130	eqtr4di	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = Id (Q) (f) (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) Id (C) (u)$
132	4	adantr	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to D \in Cat$
133		eqid	$⊢ ⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩ = ⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩$
134	20 91 124 122 126	catidcl	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) \in (f (C Nat D) f)$
135	5 6 125 123 127	catidcl	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (C) (u) \in (u Hom (C) u)$
136	1 123 132 5 6 7 8 126 126 127 127 133 134 135	evlf2val	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) Id (C) (u) = Id (Q) (f) (u) (⟨1^{st} (f) (u), 1^{st} (f) (u)⟩ comp (D) 1^{st} (f) (u)) (u 2^{nd} (f) u) (Id (C) (u))$
137	30 126 32	sylancr	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
138	5 22 137	funcf1	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to 1^{st} (f) : {Base}_{C} ⟶ {Base}_{D}$
139	138 127	ffvelrnd	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to 1^{st} (f) (u) \in {Base}_{D}$
140	22 24 26 132 139	catidcl	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (D) (1^{st} (f) (u)) \in (1^{st} (f) (u) Hom (D) 1^{st} (f) (u))$
141	22 24 26 132 139 7 139 140	catlid	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (D) (1^{st} (f) (u)) (⟨1^{st} (f) (u), 1^{st} (f) (u)⟩ comp (D) 1^{st} (f) (u)) Id (D) (1^{st} (f) (u)) = Id (D) (1^{st} (f) (u))$
142	2 124 26 126	fucid	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) = Id (D) \circ 1^{st} (f)$
143	142	fveq1d	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) (u) = (Id (D) \circ 1^{st} (f)) (u)$
144		fvco3	$⊢ (1^{st} (f) : {Base}_{C} ⟶ {Base}_{D} \land u \in {Base}_{C}) \to (Id (D) \circ 1^{st} (f)) (u) = Id (D) (1^{st} (f) (u))$
145	138 127 144	syl2anc	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to (Id (D) \circ 1^{st} (f)) (u) = Id (D) (1^{st} (f) (u))$
146	143 145	eqtrd	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) (u) = Id (D) (1^{st} (f) (u))$
147	5 125 26 137 127	funcid	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to (u 2^{nd} (f) u) (Id (C) (u)) = Id (D) (1^{st} (f) (u))$
148	146 147	oveq12d	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) (u) (⟨1^{st} (f) (u), 1^{st} (f) (u)⟩ comp (D) 1^{st} (f) (u)) (u 2^{nd} (f) u) (Id (C) (u)) = Id (D) (1^{st} (f) (u)) (⟨1^{st} (f) (u), 1^{st} (f) (u)⟩ comp (D) 1^{st} (f) (u)) Id (D) (1^{st} (f) (u))$
149	1 123 132 5 126 127	evlf1	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to f 1^{st} (E) u = 1^{st} (f) (u)$
150	149	fveq2d	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (D) (f 1^{st} (E) u) = Id (D) (1^{st} (f) (u))$
151	141 148 150	3eqtr4d	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to Id (Q) (f) (u) (⟨1^{st} (f) (u), 1^{st} (f) (u)⟩ comp (D) 1^{st} (f) (u)) (u 2^{nd} (f) u) (Id (C) (u)) = Id (D) (f 1^{st} (E) u)$
152	131 136 151	3eqtrd	$⊢ (φ \land (f \in (C Func D) \land u \in {Base}_{C})) \to (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = Id (D) (f 1^{st} (E) u)$
153	152	ralrimivva	$⊢ φ \to \forall f \in (C Func D) \forall u \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = Id (D) (f 1^{st} (E) u)$
154		id	$⊢ x = ⟨f, u⟩ \to x = ⟨f, u⟩$
155	154 154	oveq12d	$⊢ x = ⟨f, u⟩ \to x 2^{nd} (E) x = ⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩$
156		fveq2	$⊢ x = ⟨f, u⟩ \to Id (Q \times_{c} C) (x) = Id (Q \times_{c} C) (⟨f, u⟩)$
157	155 156	fveq12d	$⊢ x = ⟨f, u⟩ \to (x 2^{nd} (E) x) (Id (Q \times_{c} C) (x)) = (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩))$
158	112	fveq2d	$⊢ x = ⟨f, u⟩ \to Id (D) (1^{st} (E) (x)) = Id (D) (f 1^{st} (E) u)$
159	157 158	eqeq12d	$⊢ x = ⟨f, u⟩ \to ((x 2^{nd} (E) x) (Id (Q \times_{c} C) (x)) = Id (D) (1^{st} (E) (x)) \leftrightarrow (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = Id (D) (f 1^{st} (E) u))$
160	159	ralxp	$⊢ \forall x \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) x) (Id (Q \times_{c} C) (x)) = Id (D) (1^{st} (E) (x)) \leftrightarrow \forall f \in (C Func D) \forall u \in {Base}_{C} (⟨f, u⟩ 2^{nd} (E) ⟨f, u⟩) (Id (Q \times_{c} C) (⟨f, u⟩)) = Id (D) (f 1^{st} (E) u)$
161	153 160	sylibr	$⊢ φ \to \forall x \in ((C Func D) \times {Base}_{C}) (x 2^{nd} (E) x) (Id (Q \times_{c} C) (x)) = Id (D) (1^{st} (E) (x))$
162	161	r19.21bi	$⊢ (φ \land x \in ((C Func D) \times {Base}_{C})) \to (x 2^{nd} (E) x) (Id (Q \times_{c} C) (x)) = Id (D) (1^{st} (E) (x))$
163	3	3ad2ant1	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to C \in Cat$
164	4	3ad2ant1	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to D \in Cat$
165		simp21	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to x \in ((C Func D) \times {Base}_{C})$
166		1st2nd2	$⊢ x \in ((C Func D) \times {Base}_{C}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
167	165 166	syl	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
168	167 165	eqeltrrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in ((C Func D) \times {Base}_{C})$
169		opelxp	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in ((C Func D) \times {Base}_{C}) \leftrightarrow (1^{st} (x) \in (C Func D) \land 2^{nd} (x) \in {Base}_{C})$
170	168 169	sylib	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (1^{st} (x) \in (C Func D) \land 2^{nd} (x) \in {Base}_{C})$
171		simp22	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to y \in ((C Func D) \times {Base}_{C})$
172		1st2nd2	$⊢ y \in ((C Func D) \times {Base}_{C}) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
173	171 172	syl	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
174	173 171	eqeltrrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (y), 2^{nd} (y)⟩ \in ((C Func D) \times {Base}_{C})$
175		opelxp	$⊢ ⟨1^{st} (y), 2^{nd} (y)⟩ \in ((C Func D) \times {Base}_{C}) \leftrightarrow (1^{st} (y) \in (C Func D) \land 2^{nd} (y) \in {Base}_{C})$
176	174 175	sylib	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (1^{st} (y) \in (C Func D) \land 2^{nd} (y) \in {Base}_{C})$
177		simp23	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to z \in ((C Func D) \times {Base}_{C})$
178		1st2nd2	$⊢ z \in ((C Func D) \times {Base}_{C}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
179	177 178	syl	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
180	179 177	eqeltrrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in ((C Func D) \times {Base}_{C})$
181		opelxp	$⊢ ⟨1^{st} (z), 2^{nd} (z)⟩ \in ((C Func D) \times {Base}_{C}) \leftrightarrow (1^{st} (z) \in (C Func D) \land 2^{nd} (z) \in {Base}_{C})$
182	180 181	sylib	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (1^{st} (z) \in (C Func D) \land 2^{nd} (z) \in {Base}_{C})$
183		simp3l	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to f \in (x Hom (Q \times_{c} C) y)$
184	19 21 91 6 23 165 171	xpchom	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to x Hom (Q \times_{c} C) y = (1^{st} (x) (C Nat D) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))$
185	183 184	eleqtrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to f \in ((1^{st} (x) (C Nat D) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)))$
186		1st2nd2	$⊢ f \in ((1^{st} (x) (C Nat D) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
187	185 186	syl	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
188	187 185	eqeltrrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (f), 2^{nd} (f)⟩ \in ((1^{st} (x) (C Nat D) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)))$
189		opelxp	$⊢ ⟨1^{st} (f), 2^{nd} (f)⟩ \in ((1^{st} (x) (C Nat D) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))) \leftrightarrow (1^{st} (f) \in (1^{st} (x) (C Nat D) 1^{st} (y)) \land 2^{nd} (f) \in (2^{nd} (x) Hom (C) 2^{nd} (y)))$
190	188 189	sylib	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (1^{st} (f) \in (1^{st} (x) (C Nat D) 1^{st} (y)) \land 2^{nd} (f) \in (2^{nd} (x) Hom (C) 2^{nd} (y)))$
191		simp3r	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to g \in (y Hom (Q \times_{c} C) z)$
192	19 21 91 6 23 171 177	xpchom	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to y Hom (Q \times_{c} C) z = (1^{st} (y) (C Nat D) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))$
193	191 192	eleqtrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to g \in ((1^{st} (y) (C Nat D) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z)))$
194		1st2nd2	$⊢ g \in ((1^{st} (y) (C Nat D) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
195	193 194	syl	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
196	195 193	eqeltrrd	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (g), 2^{nd} (g)⟩ \in ((1^{st} (y) (C Nat D) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z)))$
197		opelxp	$⊢ ⟨1^{st} (g), 2^{nd} (g)⟩ \in ((1^{st} (y) (C Nat D) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))) \leftrightarrow (1^{st} (g) \in (1^{st} (y) (C Nat D) 1^{st} (z)) \land 2^{nd} (g) \in (2^{nd} (y) Hom (C) 2^{nd} (z)))$
198	196 197	sylib	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (1^{st} (g) \in (1^{st} (y) (C Nat D) 1^{st} (z)) \land 2^{nd} (g) \in (2^{nd} (y) Hom (C) 2^{nd} (z)))$
199	1 2 163 164 8 170 176 182 190 198	evlfcllem	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩ (⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (Q \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩) ⟨1^{st} (f), 2^{nd} (f)⟩) = (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩) (⟨1^{st} (E) (⟨1^{st} (x), 2^{nd} (x)⟩), 1^{st} (E) (⟨1^{st} (y), 2^{nd} (y)⟩)⟩ comp (D) 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (y), 2^{nd} (y)⟩) (⟨1^{st} (f), 2^{nd} (f)⟩)$
200	167 179	oveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to x 2^{nd} (E) z = ⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩$
201	167 173	opeq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨x, y⟩ = ⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩$
202	201 179	oveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨x, y⟩ comp (Q \times_{c} C) z = ⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (Q \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩$
203	202 195 187	oveq123d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to g (⟨x, y⟩ comp (Q \times_{c} C) z) f = ⟨1^{st} (g), 2^{nd} (g)⟩ (⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (Q \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩) ⟨1^{st} (f), 2^{nd} (f)⟩$
204	200 203	fveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (x 2^{nd} (E) z) (g (⟨x, y⟩ comp (Q \times_{c} C) z) f) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩ (⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (Q \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩) ⟨1^{st} (f), 2^{nd} (f)⟩)$
205	167	fveq2d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to 1^{st} (E) (x) = 1^{st} (E) (⟨1^{st} (x), 2^{nd} (x)⟩)$
206	173	fveq2d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to 1^{st} (E) (y) = 1^{st} (E) (⟨1^{st} (y), 2^{nd} (y)⟩)$
207	205 206	opeq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (E) (x), 1^{st} (E) (y)⟩ = ⟨1^{st} (E) (⟨1^{st} (x), 2^{nd} (x)⟩), 1^{st} (E) (⟨1^{st} (y), 2^{nd} (y)⟩)⟩$
208	179	fveq2d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to 1^{st} (E) (z) = 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)$
209	207 208	oveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to ⟨1^{st} (E) (x), 1^{st} (E) (y)⟩ comp (D) 1^{st} (E) (z) = ⟨1^{st} (E) (⟨1^{st} (x), 2^{nd} (x)⟩), 1^{st} (E) (⟨1^{st} (y), 2^{nd} (y)⟩)⟩ comp (D) 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)$
210	173 179	oveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to y 2^{nd} (E) z = ⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩$
211	210 195	fveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (y 2^{nd} (E) z) (g) = (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
212	167 173	oveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to x 2^{nd} (E) y = ⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (y), 2^{nd} (y)⟩$
213	212 187	fveq12d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (x 2^{nd} (E) y) (f) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (y), 2^{nd} (y)⟩) (⟨1^{st} (f), 2^{nd} (f)⟩)$
214	209 211 213	oveq123d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (y 2^{nd} (E) z) (g) (⟨1^{st} (E) (x), 1^{st} (E) (y)⟩ comp (D) 1^{st} (E) (z)) (x 2^{nd} (E) y) (f) = (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (E) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩) (⟨1^{st} (E) (⟨1^{st} (x), 2^{nd} (x)⟩), 1^{st} (E) (⟨1^{st} (y), 2^{nd} (y)⟩)⟩ comp (D) 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (E) ⟨1^{st} (y), 2^{nd} (y)⟩) (⟨1^{st} (f), 2^{nd} (f)⟩)$
215	199 204 214	3eqtr4d	$⊢ (φ \land (x \in ((C Func D) \times {Base}_{C}) \land y \in ((C Func D) \times {Base}_{C}) \land z \in ((C Func D) \times {Base}_{C})) \land (f \in (x Hom (Q \times_{c} C) y) \land g \in (y Hom (Q \times_{c} C) z))) \to (x 2^{nd} (E) z) (g (⟨x, y⟩ comp (Q \times_{c} C) z) f) = (y 2^{nd} (E) z) (g) (⟨1^{st} (E) (x), 1^{st} (E) (y)⟩ comp (D) 1^{st} (E) (z)) (x 2^{nd} (E) y) (f)$
216	21 22 23 24 25 26 27 7 29 4 44 55 121 162 215	isfuncd	$⊢ φ \to 1^{st} (E) ((Q \times_{c} C) Func D) 2^{nd} (E)$
217		df-br	$⊢ 1^{st} (E) ((Q \times_{c} C) Func D) 2^{nd} (E) \leftrightarrow ⟨1^{st} (E), 2^{nd} (E)⟩ \in ((Q \times_{c} C) Func D)$
218	216 217	sylib	$⊢ φ \to ⟨1^{st} (E), 2^{nd} (E)⟩ \in ((Q \times_{c} C) Func D)$
219	18 218	eqeltrd	$⊢ φ \to E \in ((Q \times_{c} C) Func D)$

Metamath Proof Explorer

Theorem evlfcl

Proof