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

Definition df-prf 17682
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 = (𝑓 ∈ V, 𝑔 ∈ V ↦ dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩)
Distinct variable group:   𝑓,𝑏,𝑔,,𝑥,𝑦

Detailed syntax breakdown of Definition df-prf
StepHypRef Expression
1 cprf 17678 . 2 class ⟨,⟩F
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cvv 3408 . . 3 class V
5 vb . . . 4 setvar 𝑏
62cv 1542 . . . . . 6 class 𝑓
7 c1st 7759 . . . . . 6 class 1st
86, 7cfv 6380 . . . . 5 class (1st𝑓)
98cdm 5551 . . . 4 class dom (1st𝑓)
10 vx . . . . . 6 setvar 𝑥
115cv 1542 . . . . . 6 class 𝑏
1210cv 1542 . . . . . . . 8 class 𝑥
1312, 8cfv 6380 . . . . . . 7 class ((1st𝑓)‘𝑥)
143cv 1542 . . . . . . . . 9 class 𝑔
1514, 7cfv 6380 . . . . . . . 8 class (1st𝑔)
1612, 15cfv 6380 . . . . . . 7 class ((1st𝑔)‘𝑥)
1713, 16cop 4547 . . . . . 6 class ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩
1810, 11, 17cmpt 5135 . . . . 5 class (𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩)
19 vy . . . . . 6 setvar 𝑦
20 vh . . . . . . 7 setvar
2119cv 1542 . . . . . . . . 9 class 𝑦
22 c2nd 7760 . . . . . . . . . 10 class 2nd
236, 22cfv 6380 . . . . . . . . 9 class (2nd𝑓)
2412, 21, 23co 7213 . . . . . . . 8 class (𝑥(2nd𝑓)𝑦)
2524cdm 5551 . . . . . . 7 class dom (𝑥(2nd𝑓)𝑦)
2620cv 1542 . . . . . . . . 9 class
2726, 24cfv 6380 . . . . . . . 8 class ((𝑥(2nd𝑓)𝑦)‘)
2814, 22cfv 6380 . . . . . . . . . 10 class (2nd𝑔)
2912, 21, 28co 7213 . . . . . . . . 9 class (𝑥(2nd𝑔)𝑦)
3026, 29cfv 6380 . . . . . . . 8 class ((𝑥(2nd𝑔)𝑦)‘)
3127, 30cop 4547 . . . . . . 7 class ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩
3220, 25, 31cmpt 5135 . . . . . 6 class ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩)
3310, 19, 11, 11, 32cmpo 7215 . . . . 5 class (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))
3418, 33cop 4547 . . . 4 class ⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩
355, 9, 34csb 3811 . . 3 class dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩
362, 3, 4, 4, 35cmpo 7215 . 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩)
371, 36wceq 1543 1 wff ⟨,⟩F = (𝑓 ∈ V, 𝑔 ∈ V ↦ dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  prfval  17706
  Copyright terms: Public domain W3C validator