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

Definition df-prf 15291
 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 15287 . 2 ⟨,⟩F
2 vf . . 3
3 vg . . 3
4 cvv 3106 . . 3
5 vb . . . 4
62cv 1373 . . . . . 6
7 c1st 6772 . . . . . 6
86, 7cfv 5579 . . . . 5
98cdm 4992 . . . 4
10 vx . . . . . 6
115cv 1373 . . . . . 6
1210cv 1373 . . . . . . . 8
1312, 8cfv 5579 . . . . . . 7
143cv 1373 . . . . . . . . 9
1514, 7cfv 5579 . . . . . . . 8
1612, 15cfv 5579 . . . . . . 7
1713, 16cop 4026 . . . . . 6
1810, 11, 17cmpt 4498 . . . . 5
19 vy . . . . . 6
20 vh . . . . . . 7
2119cv 1373 . . . . . . . . 9
22 c2nd 6773 . . . . . . . . . 10
236, 22cfv 5579 . . . . . . . . 9
2412, 21, 23co 6275 . . . . . . . 8
2524cdm 4992 . . . . . . 7
2620cv 1373 . . . . . . . . 9
2726, 24cfv 5579 . . . . . . . 8
2814, 22cfv 5579 . . . . . . . . . 10
2912, 21, 28co 6275 . . . . . . . . 9
3026, 29cfv 5579 . . . . . . . 8
3127, 30cop 4026 . . . . . . 7
3220, 25, 31cmpt 4498 . . . . . 6
3310, 19, 11, 11, 32cmpt2 6277 . . . . 5
3418, 33cop 4026 . . . 4
355, 9, 34csb 3428 . . 3
362, 3, 4, 4, 35cmpt2 6277 . 2
371, 36wceq 1374 1 ⟨,⟩F
 Colors of variables: wff setvar class This definition is referenced by:  prfval  15315
 Copyright terms: Public domain W3C validator