Definition df-prf 16815

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

Assertion

Ref	Expression
df-prf	|- ⟨,⟩F = ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. )

Distinct variable group:   f, b, g, h, x, y

Detailed syntax breakdown of Definition df-prf

Step	Hyp	Ref	Expression
1		cprf 16811	. 2 class ⟨,⟩F
2		vf	. . 3 setvar f
3		vg	. . 3 setvar g
4		cvv 3200	. . 3 class _V
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . . 6 class f
7		c1st 7166	. . . . . 6 class 1st
8	6, 7	cfv 5888	. . . . 5 class ( 1st ` f )
9	8	cdm 5114	. . . 4 class dom ( 1st ` f )
10		vx	. . . . . 6 setvar x
11	5	cv 1482	. . . . . 6 class b
12	10	cv 1482	. . . . . . . 8 class x
13	12, 8	cfv 5888	. . . . . . 7 class ( ( 1st ` f ) ` x )
14	3	cv 1482	. . . . . . . . 9 class g
15	14, 7	cfv 5888	. . . . . . . 8 class ( 1st ` g )
16	12, 15	cfv 5888	. . . . . . 7 class ( ( 1st ` g ) ` x )
17	13, 16	cop 4183	. . . . . 6 class <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >.
18	10, 11, 17	cmpt 4729	. . . . 5 class ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. )
19		vy	. . . . . 6 setvar y
20		vh	. . . . . . 7 setvar h
21	19	cv 1482	. . . . . . . . 9 class y
22		c2nd 7167	. . . . . . . . . 10 class 2nd
23	6, 22	cfv 5888	. . . . . . . . 9 class ( 2nd ` f )
24	12, 21, 23	co 6650	. . . . . . . 8 class ( x ( 2nd ` f ) y )
25	24	cdm 5114	. . . . . . 7 class dom ( x ( 2nd ` f ) y )
26	20	cv 1482	. . . . . . . . 9 class h
27	26, 24	cfv 5888	. . . . . . . 8 class ( ( x ( 2nd ` f ) y ) ` h )
28	14, 22	cfv 5888	. . . . . . . . . 10 class ( 2nd ` g )
29	12, 21, 28	co 6650	. . . . . . . . 9 class ( x ( 2nd ` g ) y )
30	26, 29	cfv 5888	. . . . . . . 8 class ( ( x ( 2nd ` g ) y ) ` h )
31	27, 30	cop 4183	. . . . . . 7 class <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >.
32	20, 25, 31	cmpt 4729	. . . . . 6 class ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. )
33	10, 19, 11, 11, 32	cmpt2 6652	. . . . 5 class ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) )
34	18, 33	cop 4183	. . . 4 class <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >.
35	5, 9, 34	csb 3533	. . 3 class [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >.
36	2, 3, 4, 4, 35	cmpt2 6652	. 2 class ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. )
37	1, 36	wceq 1483	1 wff ⟨,⟩F = ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. )

This definition is referenced by:  prfval  16839