This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑠 ) ) 𝑦 ) ) ) ⟩ )