Metamath Proof Explorer


Definition df-2ndf

Description: Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-2ndf 2ndF = ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⟨ ( 2nd𝑏 ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2ndf 2ndF
1 vr 𝑟
2 ccat Cat
3 vs 𝑠
4 cbs Base
5 1 cv 𝑟
6 5 4 cfv ( Base ‘ 𝑟 )
7 3 cv 𝑠
8 7 4 cfv ( Base ‘ 𝑠 )
9 6 8 cxp ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) )
10 vb 𝑏
11 c2nd 2nd
12 10 cv 𝑏
13 11 12 cres ( 2nd𝑏 )
14 vx 𝑥
15 vy 𝑦
16 14 cv 𝑥
17 chom Hom
18 cxpc ×c
19 5 7 18 co ( 𝑟 ×c 𝑠 )
20 19 17 cfv ( Hom ‘ ( 𝑟 ×c 𝑠 ) )
21 15 cv 𝑦
22 16 21 20 co ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 )
23 11 22 cres ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) )
24 14 15 12 12 23 cmpo ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) )
25 13 24 cop ⟨ ( 2nd𝑏 ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩
26 10 9 25 csb ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⟨ ( 2nd𝑏 ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩
27 1 3 2 2 26 cmpo ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⟨ ( 2nd𝑏 ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩ )
28 0 27 wceq 2ndF = ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⟨ ( 2nd𝑏 ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩ )