df-prf

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

		Ref	Expression
	Assertion	df-prf	⊢ ⟨,⟩_F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprf	⊢ ⟨,⟩_F
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vg	⊢ 𝑔
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑓
6	5 4	cfv	⊢ ( 1^st ‘ 𝑓 )
7	6	cdm	⊢ dom ( 1^st ‘ 𝑓 )
8		vb	⊢ 𝑏
9		vx	⊢ 𝑥
10	8	cv	⊢ 𝑏
11	9	cv	⊢ 𝑥
12	11 6	cfv	⊢ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 )
13	3	cv	⊢ 𝑔
14	13 4	cfv	⊢ ( 1^st ‘ 𝑔 )
15	11 14	cfv	⊢ ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 )
16	12 15	cop	⊢ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩
17	9 10 16	cmpt	⊢ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ )
18		vy	⊢ 𝑦
19		vh	⊢ ℎ
20		c2nd	⊢ 2^nd
21	5 20	cfv	⊢ ( 2^nd ‘ 𝑓 )
22	18	cv	⊢ 𝑦
23	11 22 21	co	⊢ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 )
24	23	cdm	⊢ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 )
25	19	cv	⊢ ℎ
26	25 23	cfv	⊢ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ )
27	13 20	cfv	⊢ ( 2^nd ‘ 𝑔 )
28	11 22 27	co	⊢ ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 )
29	25 28	cfv	⊢ ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ )
30	26 29	cop	⊢ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩
31	19 24 30	cmpt	⊢ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ )
32	9 18 10 10 31	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
33	17 32	cop	⊢ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩
34	8 7 33	csb	⊢ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩
35	1 3 2 2 34	cmpo	⊢ ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
36	0 35	wceq	⊢ ⟨,⟩_F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⦋ dom ( 1^st ‘ 𝑓 ) / 𝑏 ⦌ ⟨ ( 𝑥 ∈ 𝑏 ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( ℎ ∈ dom ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )

Metamath Proof Explorer

Definition df-prf

Detailed syntax breakdown