Definition df-prf

Description: Define the pairing operation for functors (which takes two functors F : C --> D and G : C --> E and produces ( F pairF G ) : C --> ( D Xc. E ) ). (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-prf	$$⊢{⟨,⟩}_F=\left(f\in \mathrm{V},g\in \mathrm{V}⟼⦋\mathrm{dom}{1}^{st}\left(f\right)/b⦌⟨\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right),\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprf	$$class{⟨,⟩}_F$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vg	$$setvarg$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarf$$
6	5 4	cfv	$$class{1}^{st}\left(f\right)$$
7	6	cdm	$$class\mathrm{dom}{1}^{st}\left(f\right)$$
8		vb	$$setvarb$$
9		vx	$$setvarx$$
10	8	cv	$$setvarb$$
11	9	cv	$$setvarx$$
12	11 6	cfv	$$class{1}^{st}\left(f\right)\left(x\right)$$
13	3	cv	$$setvarg$$
14	13 4	cfv	$$class{1}^{st}\left(g\right)$$
15	11 14	cfv	$$class{1}^{st}\left(g\right)\left(x\right)$$
16	12 15	cop	$$class⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩$$
17	9 10 16	cmpt	$$class\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right)$$
18		vy	$$setvary$$
19		vh	$$setvarh$$
20		c2nd	$$class{2}^{nd}$$
21	5 20	cfv	$$class{2}^{nd}\left(f\right)$$
22	18	cv	$$setvary$$
23	11 22 21	co	$$class\left(x{2}^{nd}\left(f\right)y\right)$$
24	23	cdm	$$class\mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)$$
25	19	cv	$$setvarh$$
26	25 23	cfv	$$class\left(x{2}^{nd}\left(f\right)y\right)\left(h\right)$$
27	13 20	cfv	$$class{2}^{nd}\left(g\right)$$
28	11 22 27	co	$$class\left(x{2}^{nd}\left(g\right)y\right)$$
29	25 28	cfv	$$class\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)$$
30	26 29	cop	$$class⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩$$
31	19 24 30	cmpt	$$class\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)$$
32	9 18 10 10 31	cmpo	$$class\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)$$
33	17 32	cop	$$class⟨\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right),\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)⟩$$
34	8 7 33	csb	$$class⦋\mathrm{dom}{1}^{st}\left(f\right)/b⦌⟨\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right),\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)⟩$$
35	1 3 2 2 34	cmpo	$$class\left(f\in \mathrm{V},g\in \mathrm{V}⟼⦋\mathrm{dom}{1}^{st}\left(f\right)/b⦌⟨\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right),\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)⟩\right)$$
36	0 35	wceq	$$wff{⟨,⟩}_F=\left(f\in \mathrm{V},g\in \mathrm{V}⟼⦋\mathrm{dom}{1}^{st}\left(f\right)/b⦌⟨\left(x\in b⟼⟨1^{st}\left(f\right)\left(x\right),1^{st}\left(g\right)\left(x\right)⟩\right),\left(x\in b,y\in b⟼\left(h\in \mathrm{dom}\left(x{2}^{nd}\left(f\right)y\right)⟼⟨\left(x{2}^{nd}\left(f\right)y\right)\left(h\right),\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)⟩\right)\right)⟩\right)$$