Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-prf Structured version   Unicode version

Definition df-prf 14274
 Description: Define the pairing operation for functors (which takes two functors and and produces ⟨,⟩F c ). (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-prf ⟨,⟩F
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-prf
StepHypRef Expression
1 cprf 14270 . 2 ⟨,⟩F
2 vf . . 3
3 vg . . 3
4 cvv 2958 . . 3
5 vb . . . 4
62cv 1652 . . . . . 6
7 c1st 6349 . . . . . 6
86, 7cfv 5456 . . . . 5
98cdm 4880 . . . 4
10 vx . . . . . 6
115cv 1652 . . . . . 6
1210cv 1652 . . . . . . . 8
1312, 8cfv 5456 . . . . . . 7
143cv 1652 . . . . . . . . 9
1514, 7cfv 5456 . . . . . . . 8
1612, 15cfv 5456 . . . . . . 7
1713, 16cop 3819 . . . . . 6
1810, 11, 17cmpt 4268 . . . . 5
19 vy . . . . . 6
20 vh . . . . . . 7
2119cv 1652 . . . . . . . . 9
22 c2nd 6350 . . . . . . . . . 10
236, 22cfv 5456 . . . . . . . . 9
2412, 21, 23co 6083 . . . . . . . 8
2524cdm 4880 . . . . . . 7
2620cv 1652 . . . . . . . . 9
2726, 24cfv 5456 . . . . . . . 8
2814, 22cfv 5456 . . . . . . . . . 10
2912, 21, 28co 6083 . . . . . . . . 9
3026, 29cfv 5456 . . . . . . . 8
3127, 30cop 3819 . . . . . . 7
3220, 25, 31cmpt 4268 . . . . . 6
3310, 19, 11, 11, 32cmpt2 6085 . . . . 5
3418, 33cop 3819 . . . 4
355, 9, 34csb 3253 . . 3
362, 3, 4, 4, 35cmpt2 6085 . 2
371, 36wceq 1653 1 ⟨,⟩F
 Colors of variables: wff set class This definition is referenced by:  prfval  14298
 Copyright terms: Public domain W3C validator