curf1cl

Description: The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curfval.a	$⊢ A = {Base}_{C}$
	curfval.c	$⊢ φ \to C \in Cat$
	curfval.d	$⊢ φ \to D \in Cat$
	curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curfval.b	$⊢ B = {Base}_{D}$
	curf1.x	$⊢ φ \to X \in A$
	curf1.k	$⊢ K = 1^{st} (G) (X)$
Assertion	curf1cl	$⊢ φ \to K \in (D Func E)$

Proof

Step	Hyp	Ref	Expression
1		curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curfval.a	$⊢ A = {Base}_{C}$
3		curfval.c	$⊢ φ \to C \in Cat$
4		curfval.d	$⊢ φ \to D \in Cat$
5		curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curfval.b	$⊢ B = {Base}_{D}$
7		curf1.x	$⊢ φ \to X \in A$
8		curf1.k	$⊢ K = 1^{st} (G) (X)$
9		eqid	$⊢ Hom (D) = Hom (D)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1 2 3 4 5 6 7 8 9 10	curf1	$⊢ φ \to K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$
12	6	fvexi	$⊢ B \in V$
13	12	mptex	$⊢ (y \in B ⟼ X 1^{st} (F) y) \in V$
14	12 12	mpoex	$⊢ (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) \in V$
15	13 14	op1std	$⊢ K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩ \to 1^{st} (K) = (y \in B ⟼ X 1^{st} (F) y)$
16	11 15	syl	$⊢ φ \to 1^{st} (K) = (y \in B ⟼ X 1^{st} (F) y)$
17	13 14	op2ndd	$⊢ K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩ \to 2^{nd} (K) = (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
18	11 17	syl	$⊢ φ \to 2^{nd} (K) = (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
19	16 18	opeq12d	$⊢ φ \to ⟨1^{st} (K), 2^{nd} (K)⟩ = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$
20	11 19	eqtr4d	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
21		eqid	$⊢ {Base}_{E} = {Base}_{E}$
22		eqid	$⊢ Hom (E) = Hom (E)$
23		eqid	$⊢ Id (D) = Id (D)$
24		eqid	$⊢ Id (E) = Id (E)$
25		eqid	$⊢ comp (D) = comp (D)$
26		eqid	$⊢ comp (E) = comp (E)$
27		funcrcl	$⊢ F \in ((C \times_{c} D) Func E) \to (C \times_{c} D \in Cat \land E \in Cat)$
28	5 27	syl	$⊢ φ \to (C \times_{c} D \in Cat \land E \in Cat)$
29	28	simprd	$⊢ φ \to E \in Cat$
30		eqid	$⊢ C \times_{c} D = C \times_{c} D$
31	30 2 6	xpcbas	$⊢ A \times B = {Base}_{(C \times_{c} D)}$
32		relfunc	$⊢ Rel ((C \times_{c} D) Func E)$
33		1st2ndbr	$⊢ (Rel ((C \times_{c} D) Func E) \land F \in ((C \times_{c} D) Func E)) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
34	32 5 33	sylancr	$⊢ φ \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
35	31 21 34	funcf1	$⊢ φ \to 1^{st} (F) : A \times B ⟶ {Base}_{E}$
36	35	adantr	$⊢ (φ \land y \in B) \to 1^{st} (F) : A \times B ⟶ {Base}_{E}$
37	7	adantr	$⊢ (φ \land y \in B) \to X \in A$
38		simpr	$⊢ (φ \land y \in B) \to y \in B$
39	36 37 38	fovcdmd	$⊢ (φ \land y \in B) \to X 1^{st} (F) y \in {Base}_{E}$
40	16 39	fmpt3d	$⊢ φ \to 1^{st} (K) : B ⟶ {Base}_{E}$
41		eqid	$⊢ (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) = (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
42		ovex	$⊢ y Hom (D) z \in V$
43	42	mptex	$⊢ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g) \in V$
44	41 43	fnmpoi	$⊢ (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) Fn (B \times B)$
45	18	fneq1d	$⊢ φ \to (2^{nd} (K) Fn (B \times B) \leftrightarrow (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) Fn (B \times B))$
46	44 45	mpbiri	$⊢ φ \to 2^{nd} (K) Fn (B \times B)$
47	18	oveqd	$⊢ φ \to y 2^{nd} (K) z = y (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) z$
48	41	ovmpt4g	$⊢ (y \in B \land z \in B \land (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g) \in V) \to y (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) z = (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)$
49	43 48	mp3an3	$⊢ (y \in B \land z \in B) \to y (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) z = (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)$
50	47 49	sylan9eq	$⊢ (φ \land (y \in B \land z \in B)) \to y 2^{nd} (K) z = (g \in (y Hom (D) z) ⟼ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)$
51		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
52	34	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
53	7	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to X \in A$
54		simplrl	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to y \in B$
55	53 54	opelxpd	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to ⟨X, y⟩ \in (A \times B)$
56		simplrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to z \in B$
57	53 56	opelxpd	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to ⟨X, z⟩ \in (A \times B)$
58	31 51 22 52 55 57	funcf2	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) : ⟨X, y⟩ Hom (C \times_{c} D) ⟨X, z⟩ ⟶ 1^{st} (F) (⟨X, y⟩) Hom (E) 1^{st} (F) (⟨X, z⟩)$
59		eqid	$⊢ Hom (C) = Hom (C)$
60	30 31 59 9 51 55 57	xpchom	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to ⟨X, y⟩ Hom (C \times_{c} D) ⟨X, z⟩ = (1^{st} (⟨X, y⟩) Hom (C) 1^{st} (⟨X, z⟩)) \times (2^{nd} (⟨X, y⟩) Hom (D) 2^{nd} (⟨X, z⟩))$
61	3	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to C \in Cat$
62	4	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to D \in Cat$
63	5	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to F \in ((C \times_{c} D) Func E)$
64	1 2 61 62 63 6 53 8 54	curf11	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (K) (y) = X 1^{st} (F) y$
65		df-ov	$⊢ X 1^{st} (F) y = 1^{st} (F) (⟨X, y⟩)$
66	64 65	eqtr2di	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (F) (⟨X, y⟩) = 1^{st} (K) (y)$
67	1 2 61 62 63 6 53 8 56	curf11	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (K) (z) = X 1^{st} (F) z$
68		df-ov	$⊢ X 1^{st} (F) z = 1^{st} (F) (⟨X, z⟩)$
69	67 68	eqtr2di	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (F) (⟨X, z⟩) = 1^{st} (K) (z)$
70	66 69	oveq12d	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (F) (⟨X, y⟩) Hom (E) 1^{st} (F) (⟨X, z⟩) = 1^{st} (K) (y) Hom (E) 1^{st} (K) (z)$
71	60 70	feq23d	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to ((⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) : ⟨X, y⟩ Hom (C \times_{c} D) ⟨X, z⟩ ⟶ 1^{st} (F) (⟨X, y⟩) Hom (E) 1^{st} (F) (⟨X, z⟩) \leftrightarrow (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) : (1^{st} (⟨X, y⟩) Hom (C) 1^{st} (⟨X, z⟩)) \times (2^{nd} (⟨X, y⟩) Hom (D) 2^{nd} (⟨X, z⟩)) ⟶ 1^{st} (K) (y) Hom (E) 1^{st} (K) (z))$
72	58 71	mpbid	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) : (1^{st} (⟨X, y⟩) Hom (C) 1^{st} (⟨X, z⟩)) \times (2^{nd} (⟨X, y⟩) Hom (D) 2^{nd} (⟨X, z⟩)) ⟶ 1^{st} (K) (y) Hom (E) 1^{st} (K) (z)$
73	2 59 10 61 53	catidcl	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to Id (C) (X) \in (X Hom (C) X)$
74		op1stg	$⊢ (X \in A \land y \in B) \to 1^{st} (⟨X, y⟩) = X$
75	53 54 74	syl2anc	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (⟨X, y⟩) = X$
76		op1stg	$⊢ (X \in A \land z \in B) \to 1^{st} (⟨X, z⟩) = X$
77	53 56 76	syl2anc	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (⟨X, z⟩) = X$
78	75 77	oveq12d	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 1^{st} (⟨X, y⟩) Hom (C) 1^{st} (⟨X, z⟩) = X Hom (C) X$
79	73 78	eleqtrrd	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to Id (C) (X) \in (1^{st} (⟨X, y⟩) Hom (C) 1^{st} (⟨X, z⟩))$
80		simpr	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to g \in (y Hom (D) z)$
81		op2ndg	$⊢ (X \in A \land y \in B) \to 2^{nd} (⟨X, y⟩) = y$
82	53 54 81	syl2anc	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 2^{nd} (⟨X, y⟩) = y$
83		op2ndg	$⊢ (X \in A \land z \in B) \to 2^{nd} (⟨X, z⟩) = z$
84	53 56 83	syl2anc	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 2^{nd} (⟨X, z⟩) = z$
85	82 84	oveq12d	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to 2^{nd} (⟨X, y⟩) Hom (D) 2^{nd} (⟨X, z⟩) = y Hom (D) z$
86	80 85	eleqtrrd	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to g \in (2^{nd} (⟨X, y⟩) Hom (D) 2^{nd} (⟨X, z⟩))$
87	72 79 86	fovcdmd	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y Hom (D) z)) \to Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g \in (1^{st} (K) (y) Hom (E) 1^{st} (K) (z))$
88	50 87	fmpt3d	$⊢ (φ \land (y \in B \land z \in B)) \to (y 2^{nd} (K) z) : y Hom (D) z ⟶ 1^{st} (K) (y) Hom (E) 1^{st} (K) (z)$
89	3	adantr	$⊢ (φ \land y \in B) \to C \in Cat$
90	4	adantr	$⊢ (φ \land y \in B) \to D \in Cat$
91		eqid	$⊢ Id (C \times_{c} D) = Id (C \times_{c} D)$
92	30 89 90 2 6 10 23 91 37 38	xpcid	$⊢ (φ \land y \in B) \to Id (C \times_{c} D) (⟨X, y⟩) = ⟨Id (C) (X), Id (D) (y)⟩$
93	92	fveq2d	$⊢ (φ \land y \in B) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) (Id (C \times_{c} D) (⟨X, y⟩)) = (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) (⟨Id (C) (X), Id (D) (y)⟩)$
94		df-ov	$⊢ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) Id (D) (y) = (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) (⟨Id (C) (X), Id (D) (y)⟩)$
95	93 94	eqtr4di	$⊢ (φ \land y \in B) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) (Id (C \times_{c} D) (⟨X, y⟩)) = Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) Id (D) (y)$
96	34	adantr	$⊢ (φ \land y \in B) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
97		opelxpi	$⊢ (X \in A \land y \in B) \to ⟨X, y⟩ \in (A \times B)$
98	7 97	sylan	$⊢ (φ \land y \in B) \to ⟨X, y⟩ \in (A \times B)$
99	31 91 24 96 98	funcid	$⊢ (φ \land y \in B) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) (Id (C \times_{c} D) (⟨X, y⟩)) = Id (E) (1^{st} (F) (⟨X, y⟩))$
100	95 99	eqtr3d	$⊢ (φ \land y \in B) \to Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) Id (D) (y) = Id (E) (1^{st} (F) (⟨X, y⟩))$
101	5	adantr	$⊢ (φ \land y \in B) \to F \in ((C \times_{c} D) Func E)$
102	6 9 23 90 38	catidcl	$⊢ (φ \land y \in B) \to Id (D) (y) \in (y Hom (D) y)$
103	1 2 89 90 101 6 37 8 38 9 10 38 102	curf12	$⊢ (φ \land y \in B) \to (y 2^{nd} (K) y) (Id (D) (y)) = Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, y⟩) Id (D) (y)$
104	1 2 89 90 101 6 37 8 38	curf11	$⊢ (φ \land y \in B) \to 1^{st} (K) (y) = X 1^{st} (F) y$
105	104 65	eqtrdi	$⊢ (φ \land y \in B) \to 1^{st} (K) (y) = 1^{st} (F) (⟨X, y⟩)$
106	105	fveq2d	$⊢ (φ \land y \in B) \to Id (E) (1^{st} (K) (y)) = Id (E) (1^{st} (F) (⟨X, y⟩))$
107	100 103 106	3eqtr4d	$⊢ (φ \land y \in B) \to (y 2^{nd} (K) y) (Id (D) (y)) = Id (E) (1^{st} (K) (y))$
108	7	3ad2ant1	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to X \in A$
109		simp21	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to y \in B$
110		simp22	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to z \in B$
111		eqid	$⊢ comp (C) = comp (C)$
112		eqid	$⊢ comp (C \times_{c} D) = comp (C \times_{c} D)$
113		simp23	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to w \in B$
114	3	3ad2ant1	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to C \in Cat$
115	2 59 10 114 108	catidcl	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to Id (C) (X) \in (X Hom (C) X)$
116		simp3l	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to g \in (y Hom (D) z)$
117		simp3r	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to h \in (z Hom (D) w)$
118	30 2 6 59 9 108 109 108 110 111 25 112 108 113 115 116 115 117	xpcco2	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), h⟩ (⟨⟨X, y⟩, ⟨X, z⟩⟩ comp (C \times_{c} D) ⟨X, w⟩) ⟨Id (C) (X), g⟩ = ⟨Id (C) (X) (⟨X, X⟩ comp (C) X) Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩$
119	2 59 10 114 108 111 108 115	catlid	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to Id (C) (X) (⟨X, X⟩ comp (C) X) Id (C) (X) = Id (C) (X)$
120	119	opeq1d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X) (⟨X, X⟩ comp (C) X) Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩ = ⟨Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩$
121	118 120	eqtrd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), h⟩ (⟨⟨X, y⟩, ⟨X, z⟩⟩ comp (C \times_{c} D) ⟨X, w⟩) ⟨Id (C) (X), g⟩ = ⟨Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩$
122	121	fveq2d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩ (⟨⟨X, y⟩, ⟨X, z⟩⟩ comp (C \times_{c} D) ⟨X, w⟩) ⟨Id (C) (X), g⟩) = (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩)$
123		df-ov	$⊢ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (h (⟨y, z⟩ comp (D) w) g) = (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h (⟨y, z⟩ comp (D) w) g⟩)$
124	122 123	eqtr4di	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩ (⟨⟨X, y⟩, ⟨X, z⟩⟩ comp (C \times_{c} D) ⟨X, w⟩) ⟨Id (C) (X), g⟩) = Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (h (⟨y, z⟩ comp (D) w) g)$
125	34	3ad2ant1	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
126	108 109	opelxpd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨X, y⟩ \in (A \times B)$
127	108 110	opelxpd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨X, z⟩ \in (A \times B)$
128	108 113	opelxpd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨X, w⟩ \in (A \times B)$
129	115 116	opelxpd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), g⟩ \in ((X Hom (C) X) \times (y Hom (D) z))$
130	30 2 6 59 9 108 109 108 110 51	xpchom2	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨X, y⟩ Hom (C \times_{c} D) ⟨X, z⟩ = (X Hom (C) X) \times (y Hom (D) z)$
131	129 130	eleqtrrd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), g⟩ \in (⟨X, y⟩ Hom (C \times_{c} D) ⟨X, z⟩)$
132	115 117	opelxpd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), h⟩ \in ((X Hom (C) X) \times (z Hom (D) w))$
133	30 2 6 59 9 108 110 108 113 51	xpchom2	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨X, z⟩ Hom (C \times_{c} D) ⟨X, w⟩ = (X Hom (C) X) \times (z Hom (D) w)$
134	132 133	eleqtrrd	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨Id (C) (X), h⟩ \in (⟨X, z⟩ Hom (C \times_{c} D) ⟨X, w⟩)$
135	31 51 112 26 125 126 127 128 131 134	funcco	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩ (⟨⟨X, y⟩, ⟨X, z⟩⟩ comp (C \times_{c} D) ⟨X, w⟩) ⟨Id (C) (X), g⟩) = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩) (⟨1^{st} (F) (⟨X, y⟩), 1^{st} (F) (⟨X, z⟩)⟩ comp (E) 1^{st} (F) (⟨X, w⟩)) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) (⟨Id (C) (X), g⟩)$
136	124 135	eqtr3d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (h (⟨y, z⟩ comp (D) w) g) = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩) (⟨1^{st} (F) (⟨X, y⟩), 1^{st} (F) (⟨X, z⟩)⟩ comp (E) 1^{st} (F) (⟨X, w⟩)) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) (⟨Id (C) (X), g⟩)$
137	4	3ad2ant1	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to D \in Cat$
138	5	3ad2ant1	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to F \in ((C \times_{c} D) Func E)$
139	6 9 25 137 109 110 113 116 117	catcocl	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to h (⟨y, z⟩ comp (D) w) g \in (y Hom (D) w)$
140	1 2 114 137 138 6 108 8 109 9 10 113 139	curf12	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (y 2^{nd} (K) w) (h (⟨y, z⟩ comp (D) w) g) = Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, w⟩) (h (⟨y, z⟩ comp (D) w) g)$
141	1 2 114 137 138 6 108 8 109	curf11	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (y) = X 1^{st} (F) y$
142	141 65	eqtrdi	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (y) = 1^{st} (F) (⟨X, y⟩)$
143	1 2 114 137 138 6 108 8 110	curf11	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (z) = X 1^{st} (F) z$
144	143 68	eqtrdi	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (z) = 1^{st} (F) (⟨X, z⟩)$
145	142 144	opeq12d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨1^{st} (K) (y), 1^{st} (K) (z)⟩ = ⟨1^{st} (F) (⟨X, y⟩), 1^{st} (F) (⟨X, z⟩)⟩$
146	1 2 114 137 138 6 108 8 113	curf11	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (w) = X 1^{st} (F) w$
147		df-ov	$⊢ X 1^{st} (F) w = 1^{st} (F) (⟨X, w⟩)$
148	146 147	eqtrdi	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to 1^{st} (K) (w) = 1^{st} (F) (⟨X, w⟩)$
149	145 148	oveq12d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to ⟨1^{st} (K) (y), 1^{st} (K) (z)⟩ comp (E) 1^{st} (K) (w) = ⟨1^{st} (F) (⟨X, y⟩), 1^{st} (F) (⟨X, z⟩)⟩ comp (E) 1^{st} (F) (⟨X, w⟩)$
150	1 2 114 137 138 6 108 8 110 9 10 113 117	curf12	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (z 2^{nd} (K) w) (h) = Id (C) (X) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) h$
151		df-ov	$⊢ Id (C) (X) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) h = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩)$
152	150 151	eqtrdi	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (z 2^{nd} (K) w) (h) = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩)$
153	1 2 114 137 138 6 108 8 109 9 10 110 116	curf12	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (y 2^{nd} (K) z) (g) = Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g$
154		df-ov	$⊢ Id (C) (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g = (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) (⟨Id (C) (X), g⟩)$
155	153 154	eqtrdi	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (y 2^{nd} (K) z) (g) = (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) (⟨Id (C) (X), g⟩)$
156	149 152 155	oveq123d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (z 2^{nd} (K) w) (h) (⟨1^{st} (K) (y), 1^{st} (K) (z)⟩ comp (E) 1^{st} (K) (w)) (y 2^{nd} (K) z) (g) = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), h⟩) (⟨1^{st} (F) (⟨X, y⟩), 1^{st} (F) (⟨X, z⟩)⟩ comp (E) 1^{st} (F) (⟨X, w⟩)) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) (⟨Id (C) (X), g⟩)$
157	136 140 156	3eqtr4d	$⊢ (φ \land (y \in B \land z \in B \land w \in B) \land (g \in (y Hom (D) z) \land h \in (z Hom (D) w))) \to (y 2^{nd} (K) w) (h (⟨y, z⟩ comp (D) w) g) = (z 2^{nd} (K) w) (h) (⟨1^{st} (K) (y), 1^{st} (K) (z)⟩ comp (E) 1^{st} (K) (w)) (y 2^{nd} (K) z) (g)$
158	6 21 9 22 23 24 25 26 4 29 40 46 88 107 157	isfuncd	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
159		df-br	$⊢ 1^{st} (K) (D Func E) 2^{nd} (K) \leftrightarrow ⟨1^{st} (K), 2^{nd} (K)⟩ \in (D Func E)$
160	158 159	sylib	$⊢ φ \to ⟨1^{st} (K), 2^{nd} (K)⟩ \in (D Func E)$
161	20 160	eqeltrd	$⊢ φ \to K \in (D Func E)$

Metamath Proof Explorer

Theorem curf1cl

Proof