curf2cl

Description: The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curf2.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curf2.a	$⊢ A = {Base}_{C}$
	curf2.c	$⊢ φ \to C \in Cat$
	curf2.d	$⊢ φ \to D \in Cat$
	curf2.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curf2.b	$⊢ B = {Base}_{D}$
	curf2.h	$⊢ H = Hom (C)$
	curf2.i	$⊢ I = Id (D)$
	curf2.x	$⊢ φ \to X \in A$
	curf2.y	$⊢ φ \to Y \in A$
	curf2.k	$⊢ φ \to K \in (X H Y)$
	curf2.l	$⊢ L = (X 2^{nd} (G) Y) (K)$
	curf2.n	$⊢ N = D Nat E$
Assertion	curf2cl	$⊢ φ \to L \in (1^{st} (G) (X) N 1^{st} (G) (Y))$

Proof

Step	Hyp	Ref	Expression
1		curf2.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curf2.a	$⊢ A = {Base}_{C}$
3		curf2.c	$⊢ φ \to C \in Cat$
4		curf2.d	$⊢ φ \to D \in Cat$
5		curf2.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curf2.b	$⊢ B = {Base}_{D}$
7		curf2.h	$⊢ H = Hom (C)$
8		curf2.i	$⊢ I = Id (D)$
9		curf2.x	$⊢ φ \to X \in A$
10		curf2.y	$⊢ φ \to Y \in A$
11		curf2.k	$⊢ φ \to K \in (X H Y)$
12		curf2.l	$⊢ L = (X 2^{nd} (G) Y) (K)$
13		curf2.n	$⊢ N = D Nat E$
14	1 2 3 4 5 6 7 8 9 10 11 12	curf2	$⊢ φ \to L = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z))$
15		eqid	$⊢ C \times_{c} D = C \times_{c} D$
16	15 2 6	xpcbas	$⊢ A \times B = {Base}_{(C \times_{c} D)}$
17		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
18		eqid	$⊢ Hom (E) = Hom (E)$
19		relfunc	$⊢ Rel ((C \times_{c} D) Func E)$
20		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)$
21	19 5 20	sylancr	$⊢ φ \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
22	21	adantr	$⊢ (φ \land z \in B) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
23		opelxpi	$⊢ (X \in A \land z \in B) \to ⟨X, z⟩ \in (A \times B)$
24	9 23	sylan	$⊢ (φ \land z \in B) \to ⟨X, z⟩ \in (A \times B)$
25		opelxpi	$⊢ (Y \in A \land z \in B) \to ⟨Y, z⟩ \in (A \times B)$
26	10 25	sylan	$⊢ (φ \land z \in B) \to ⟨Y, z⟩ \in (A \times B)$
27	16 17 18 22 24 26	funcf2	$⊢ (φ \land z \in B) \to (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) : ⟨X, z⟩ Hom (C \times_{c} D) ⟨Y, z⟩ ⟶ 1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩)$
28		eqid	$⊢ Hom (D) = Hom (D)$
29	9	adantr	$⊢ (φ \land z \in B) \to X \in A$
30		simpr	$⊢ (φ \land z \in B) \to z \in B$
31	10	adantr	$⊢ (φ \land z \in B) \to Y \in A$
32	15 2 6 7 28 29 30 31 30 17	xpchom2	$⊢ (φ \land z \in B) \to ⟨X, z⟩ Hom (C \times_{c} D) ⟨Y, z⟩ = (X H Y) \times (z Hom (D) z)$
33	32	feq2d	$⊢ (φ \land z \in B) \to ((⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) : ⟨X, z⟩ Hom (C \times_{c} D) ⟨Y, z⟩ ⟶ 1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩) \leftrightarrow (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) : (X H Y) \times (z Hom (D) z) ⟶ 1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩))$
34	27 33	mpbid	$⊢ (φ \land z \in B) \to (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) : (X H Y) \times (z Hom (D) z) ⟶ 1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩)$
35	11	adantr	$⊢ (φ \land z \in B) \to K \in (X H Y)$
36	4	adantr	$⊢ (φ \land z \in B) \to D \in Cat$
37	6 28 8 36 30	catidcl	$⊢ (φ \land z \in B) \to I (z) \in (z Hom (D) z)$
38	34 35 37	fovcdmd	$⊢ (φ \land z \in B) \to K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) \in (1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩))$
39	3	adantr	$⊢ (φ \land z \in B) \to C \in Cat$
40	5	adantr	$⊢ (φ \land z \in B) \to F \in ((C \times_{c} D) Func E)$
41		eqid	$⊢ 1^{st} (G) (X) = 1^{st} (G) (X)$
42	1 2 39 36 40 6 29 41 30	curf11	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (G) (X)) (z) = X 1^{st} (F) z$
43		df-ov	$⊢ X 1^{st} (F) z = 1^{st} (F) (⟨X, z⟩)$
44	42 43	eqtrdi	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (G) (X)) (z) = 1^{st} (F) (⟨X, z⟩)$
45		eqid	$⊢ 1^{st} (G) (Y) = 1^{st} (G) (Y)$
46	1 2 39 36 40 6 31 45 30	curf11	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (G) (Y)) (z) = Y 1^{st} (F) z$
47		df-ov	$⊢ Y 1^{st} (F) z = 1^{st} (F) (⟨Y, z⟩)$
48	46 47	eqtrdi	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (G) (Y)) (z) = 1^{st} (F) (⟨Y, z⟩)$
49	44 48	oveq12d	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z) = 1^{st} (F) (⟨X, z⟩) Hom (E) 1^{st} (F) (⟨Y, z⟩)$
50	38 49	eleqtrrd	$⊢ (φ \land z \in B) \to K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) \in (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z))$
51	50	ralrimiva	$⊢ φ \to \forall z \in B K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) \in (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z))$
52	6	fvexi	$⊢ B \in V$
53		mptelixpg	$⊢ B \in V \to ((z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z)) \leftrightarrow \forall z \in B K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) \in (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z)))$
54	52 53	ax-mp	$⊢ (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z)) \leftrightarrow \forall z \in B K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) \in (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z))$
55	51 54	sylibr	$⊢ φ \to (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z))$
56	14 55	eqeltrd	$⊢ φ \to L \in \underset{z \in B}{⨉} (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z))$
57		eqid	$⊢ Id (C) = Id (C)$
58	3	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to C \in Cat$
59	9	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to X \in A$
60		eqid	$⊢ comp (C) = comp (C)$
61	10	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to Y \in A$
62	11	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to K \in (X H Y)$
63	2 7 57 58 59 60 61 62	catrid	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to K (⟨X, X⟩ comp (C) Y) Id (C) (X) = K$
64	2 7 57 58 59 60 61 62	catlid	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to Id (C) (Y) (⟨X, Y⟩ comp (C) Y) K = K$
65	63 64	eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to K (⟨X, X⟩ comp (C) Y) Id (C) (X) = Id (C) (Y) (⟨X, Y⟩ comp (C) Y) K$
66	4	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to D \in Cat$
67		simpr1	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to z \in B$
68		eqid	$⊢ comp (D) = comp (D)$
69		simpr2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to w \in B$
70		simpr3	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to f \in (z Hom (D) w)$
71	6 28 8 66 67 68 69 70	catlid	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to I (w) (⟨z, w⟩ comp (D) w) f = f$
72	6 28 8 66 67 68 69 70	catrid	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to f (⟨z, z⟩ comp (D) w) I (z) = f$
73	71 72	eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to I (w) (⟨z, w⟩ comp (D) w) f = f (⟨z, z⟩ comp (D) w) I (z)$
74	65 73	opeq12d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K (⟨X, X⟩ comp (C) Y) Id (C) (X), I (w) (⟨z, w⟩ comp (D) w) f⟩ = ⟨Id (C) (Y) (⟨X, Y⟩ comp (C) Y) K, f (⟨z, z⟩ comp (D) w) I (z)⟩$
75		eqid	$⊢ comp (C \times_{c} D) = comp (C \times_{c} D)$
76	2 7 57 58 59	catidcl	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to Id (C) (X) \in (X H X)$
77	6 28 8 66 69	catidcl	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to I (w) \in (w Hom (D) w)$
78	15 2 6 7 28 59 67 59 69 60 68 75 61 69 76 70 62 77	xpcco2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (w)⟩ (⟨⟨X, z⟩, ⟨X, w⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨Id (C) (X), f⟩ = ⟨K (⟨X, X⟩ comp (C) Y) Id (C) (X), I (w) (⟨z, w⟩ comp (D) w) f⟩$
79	37	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to I (z) \in (z Hom (D) z)$
80	2 7 57 58 61	catidcl	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to Id (C) (Y) \in (Y H Y)$
81	15 2 6 7 28 59 67 61 67 60 68 75 61 69 62 79 80 70	xpcco2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Id (C) (Y), f⟩ (⟨⟨X, z⟩, ⟨Y, z⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨K, I (z)⟩ = ⟨Id (C) (Y) (⟨X, Y⟩ comp (C) Y) K, f (⟨z, z⟩ comp (D) w) I (z)⟩$
82	74 78 81	3eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (w)⟩ (⟨⟨X, z⟩, ⟨X, w⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨Id (C) (X), f⟩ = ⟨Id (C) (Y), f⟩ (⟨⟨X, z⟩, ⟨Y, z⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨K, I (z)⟩$
83	82	fveq2d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (⟨X, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩ (⟨⟨X, z⟩, ⟨X, w⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨Id (C) (X), f⟩) = (⟨X, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩ (⟨⟨X, z⟩, ⟨Y, z⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨K, I (z)⟩)$
84		eqid	$⊢ comp (E) = comp (E)$
85	21	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
86	24	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨X, z⟩ \in (A \times B)$
87	59 69	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨X, w⟩ \in (A \times B)$
88	61 69	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Y, w⟩ \in (A \times B)$
89	76 70	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Id (C) (X), f⟩ \in ((X H X) \times (z Hom (D) w))$
90	15 2 6 7 28 59 67 59 69 17	xpchom2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨X, z⟩ Hom (C \times_{c} D) ⟨X, w⟩ = (X H X) \times (z Hom (D) w)$
91	89 90	eleqtrrd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Id (C) (X), f⟩ \in (⟨X, z⟩ Hom (C \times_{c} D) ⟨X, w⟩)$
92	62 77	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (w)⟩ \in ((X H Y) \times (w Hom (D) w))$
93	15 2 6 7 28 59 69 61 69 17	xpchom2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨X, w⟩ Hom (C \times_{c} D) ⟨Y, w⟩ = (X H Y) \times (w Hom (D) w)$
94	92 93	eleqtrrd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (w)⟩ \in (⟨X, w⟩ Hom (C \times_{c} D) ⟨Y, w⟩)$
95	16 17 75 84 85 86 87 88 91 94	funcco	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (⟨X, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩ (⟨⟨X, z⟩, ⟨X, w⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨Id (C) (X), f⟩) = (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨X, w⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), f⟩)$
96	26	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Y, z⟩ \in (A \times B)$
97	62 79	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (z)⟩ \in ((X H Y) \times (z Hom (D) z))$
98	15 2 6 7 28 59 67 61 67 17	xpchom2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨X, z⟩ Hom (C \times_{c} D) ⟨Y, z⟩ = (X H Y) \times (z Hom (D) z)$
99	97 98	eleqtrrd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨K, I (z)⟩ \in (⟨X, z⟩ Hom (C \times_{c} D) ⟨Y, z⟩)$
100	80 70	opelxpd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Id (C) (Y), f⟩ \in ((Y H Y) \times (z Hom (D) w))$
101	15 2 6 7 28 61 67 61 69 17	xpchom2	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Y, z⟩ Hom (C \times_{c} D) ⟨Y, w⟩ = (Y H Y) \times (z Hom (D) w)$
102	100 101	eleqtrrd	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨Id (C) (Y), f⟩ \in (⟨Y, z⟩ Hom (C \times_{c} D) ⟨Y, w⟩)$
103	16 17 75 84 85 86 96 88 99 102	funcco	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (⟨X, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩ (⟨⟨X, z⟩, ⟨Y, z⟩⟩ comp (C \times_{c} D) ⟨Y, w⟩) ⟨K, I (z)⟩) = (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨Y, z⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) (⟨K, I (z)⟩)$
104	83 95 103	3eqtr3d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨X, w⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), f⟩) = (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨Y, z⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) (⟨K, I (z)⟩)$
105	5	adantr	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to F \in ((C \times_{c} D) Func E)$
106	1 2 58 66 105 6 59 41 67	curf11	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (X)) (z) = X 1^{st} (F) z$
107	106 43	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (X)) (z) = 1^{st} (F) (⟨X, z⟩)$
108	1 2 58 66 105 6 59 41 69	curf11	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (X)) (w) = X 1^{st} (F) w$
109		df-ov	$⊢ X 1^{st} (F) w = 1^{st} (F) (⟨X, w⟩)$
110	108 109	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (X)) (w) = 1^{st} (F) (⟨X, w⟩)$
111	107 110	opeq12d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ = ⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨X, w⟩)⟩$
112	1 2 58 66 105 6 61 45 69	curf11	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (Y)) (w) = Y 1^{st} (F) w$
113		df-ov	$⊢ Y 1^{st} (F) w = 1^{st} (F) (⟨Y, w⟩)$
114	112 113	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (Y)) (w) = 1^{st} (F) (⟨Y, w⟩)$
115	111 114	oveq12d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w) = ⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨X, w⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)$
116	1 2 58 66 105 6 7 8 59 61 62 12 69	curf2val	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (w) = K (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) I (w)$
117		df-ov	$⊢ K (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) I (w) = (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩)$
118	116 117	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (w) = (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩)$
119	1 2 58 66 105 6 59 41 67 28 57 69 70	curf12	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (z 2^{nd} (1^{st} (G) (X)) w) (f) = Id (C) (X) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) f$
120		df-ov	$⊢ Id (C) (X) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) f = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), f⟩)$
121	119 120	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (z 2^{nd} (1^{st} (G) (X)) w) (f) = (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), f⟩)$
122	115 118 121	oveq123d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (w) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) (z 2^{nd} (1^{st} (G) (X)) w) (f) = (⟨X, w⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨K, I (w)⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨X, w⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨X, w⟩) (⟨Id (C) (X), f⟩)$
123	1 2 58 66 105 6 61 45 67	curf11	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (Y)) (z) = Y 1^{st} (F) z$
124	123 47	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to 1^{st} (1^{st} (G) (Y)) (z) = 1^{st} (F) (⟨Y, z⟩)$
125	107 124	opeq12d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ = ⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨Y, z⟩)⟩$
126	125 114	oveq12d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w) = ⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨Y, z⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)$
127	1 2 58 66 105 6 61 45 67 28 57 69 70	curf12	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (z 2^{nd} (1^{st} (G) (Y)) w) (f) = Id (C) (Y) (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) f$
128		df-ov	$⊢ Id (C) (Y) (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) f = (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩)$
129	127 128	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (z 2^{nd} (1^{st} (G) (Y)) w) (f) = (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩)$
130	1 2 58 66 105 6 7 8 59 61 62 12 67	curf2val	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (z) = K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)$
131		df-ov	$⊢ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z) = (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) (⟨K, I (z)⟩)$
132	130 131	eqtrdi	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (z) = (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) (⟨K, I (z)⟩)$
133	126 129 132	oveq123d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to (z 2^{nd} (1^{st} (G) (Y)) w) (f) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) L (z) = (⟨Y, z⟩ 2^{nd} (F) ⟨Y, w⟩) (⟨Id (C) (Y), f⟩) (⟨1^{st} (F) (⟨X, z⟩), 1^{st} (F) (⟨Y, z⟩)⟩ comp (E) 1^{st} (F) (⟨Y, w⟩)) (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) (⟨K, I (z)⟩)$
134	104 122 133	3eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land f \in (z Hom (D) w))) \to L (w) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) (z 2^{nd} (1^{st} (G) (X)) w) (f) = (z 2^{nd} (1^{st} (G) (Y)) w) (f) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) L (z)$
135	134	ralrimivvva	$⊢ φ \to \forall z \in B \forall w \in B \forall f \in (z Hom (D) w) L (w) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) (z 2^{nd} (1^{st} (G) (X)) w) (f) = (z 2^{nd} (1^{st} (G) (Y)) w) (f) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) L (z)$
136	1 2 3 4 5 6 9 41	curf1cl	$⊢ φ \to 1^{st} (G) (X) \in (D Func E)$
137	1 2 3 4 5 6 10 45	curf1cl	$⊢ φ \to 1^{st} (G) (Y) \in (D Func E)$
138	13 6 28 18 84 136 137	isnat2	$⊢ φ \to (L \in (1^{st} (G) (X) N 1^{st} (G) (Y)) \leftrightarrow (L \in \underset{z \in B}{⨉} (1^{st} (1^{st} (G) (X)) (z) Hom (E) 1^{st} (1^{st} (G) (Y)) (z)) \land \forall z \in B \forall w \in B \forall f \in (z Hom (D) w) L (w) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (X)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) (z 2^{nd} (1^{st} (G) (X)) w) (f) = (z 2^{nd} (1^{st} (G) (Y)) w) (f) (⟨1^{st} (1^{st} (G) (X)) (z), 1^{st} (1^{st} (G) (Y)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (Y)) (w)) L (z)))$
139	56 135 138	mpbir2and	$⊢ φ \to L \in (1^{st} (G) (X) N 1^{st} (G) (Y))$

Metamath Proof Explorer

Theorem curf2cl

Proof