Definition df-prf 17892

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

Step	Hyp	Ref	Expression
1		cprf 17888	. 2 class ⟨,⟩F
2		vf	. . 3 setvar 𝑓
3		vg	. . 3 setvar 𝑔
4		cvv 3432	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1538	. . . . . 6 class 𝑓
7		c1st 7829	. . . . . 6 class 1st
8	6, 7	cfv 6433	. . . . 5 class (1st ‘𝑓)
9	8	cdm 5589	. . . 4 class dom (1st ‘𝑓)
10		vx	. . . . . 6 setvar 𝑥
11	5	cv 1538	. . . . . 6 class 𝑏
12	10	cv 1538	. . . . . . . 8 class 𝑥
13	12, 8	cfv 6433	. . . . . . 7 class ((1st ‘𝑓)‘𝑥)
14	3	cv 1538	. . . . . . . . 9 class 𝑔
15	14, 7	cfv 6433	. . . . . . . 8 class (1st ‘𝑔)
16	12, 15	cfv 6433	. . . . . . 7 class ((1st ‘𝑔)‘𝑥)
17	13, 16	cop 4567	. . . . . 6 class ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩
18	10, 11, 17	cmpt 5157	. . . . 5 class (𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩)
19		vy	. . . . . 6 setvar 𝑦
20		vh	. . . . . . 7 setvar ℎ
21	19	cv 1538	. . . . . . . . 9 class 𝑦
22		c2nd 7830	. . . . . . . . . 10 class 2nd
23	6, 22	cfv 6433	. . . . . . . . 9 class (2nd ‘𝑓)
24	12, 21, 23	co 7275	. . . . . . . 8 class (𝑥(2nd ‘𝑓)𝑦)
25	24	cdm 5589	. . . . . . 7 class dom (𝑥(2nd ‘𝑓)𝑦)
26	20	cv 1538	. . . . . . . . 9 class ℎ
27	26, 24	cfv 6433	. . . . . . . 8 class ((𝑥(2nd ‘𝑓)𝑦)‘ℎ)
28	14, 22	cfv 6433	. . . . . . . . . 10 class (2nd ‘𝑔)
29	12, 21, 28	co 7275	. . . . . . . . 9 class (𝑥(2nd ‘𝑔)𝑦)
30	26, 29	cfv 6433	. . . . . . . 8 class ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)
31	27, 30	cop 4567	. . . . . . 7 class ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩
32	20, 25, 31	cmpt 5157	. . . . . 6 class (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩)
33	10, 19, 11, 11, 32	cmpo 7277	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))
34	18, 33	cop 4567	. . . 4 class ⟨(𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))⟩
35	5, 9, 34	csb 3832	. . 3 class ⦋dom (1st ‘𝑓) / 𝑏⦌⟨(𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))⟩
36	2, 3, 4, 4, 35	cmpo 7277	. 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ ⦋dom (1st ‘𝑓) / 𝑏⦌⟨(𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))⟩)
37	1, 36	wceq 1539	1 wff ⟨,⟩F = (𝑓 ∈ V, 𝑔 ∈ V ↦ ⦋dom (1st ‘𝑓) / 𝑏⦌⟨(𝑥 ∈ 𝑏 ↦ ⟨((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)⟩), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ ⟨((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)⟩))⟩)

This definition is referenced by:  prfval  17916