prfcl

Description: The pairing of functors F : C --> D and G : C --> D is a functor <. F , G >. : C --> ( D X. E ) . (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfcl.p	$⊢ P = F {⟨,⟩}_{F} G$
	prfcl.t	$⊢ T = D \times_{c} E$
	prfcl.c	$⊢ φ \to F \in (C Func D)$
	prfcl.d	$⊢ φ \to G \in (C Func E)$
Assertion	prfcl	$⊢ φ \to P \in (C Func T)$

Proof

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

Metamath Proof Explorer

Theorem prfcl

Proof