Metamath Proof Explorer

Definition df-mon

Description: Function returning the monomorphisms of the category c . JFM CAT_1 def. 10. (Contributed by FL, 5-Dec-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-mon Mono = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmon ⊢ Mono
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 cbs ⊢ Base
4 1 cv ⊢ 𝑐
5 4 3 cfv ⊢ ( Base ‘ 𝑐 )
6 vb ⊢ 𝑏
7 chom ⊢ Hom
8 4 7 cfv ⊢ ( Hom ‘ 𝑐 )
9 vh ⊢ ℎ
10 vx ⊢ 𝑥
11 6 cv ⊢ 𝑏
12 vy ⊢ 𝑦
13 vf ⊢ 𝑓
14 10 cv ⊢ 𝑥
15 9 cv ⊢ ℎ
16 12 cv ⊢ 𝑦
17 14 16 15 co ⊢ ( 𝑥 ℎ 𝑦 )
18 vz ⊢ 𝑧
19 vg ⊢ 𝑔
20 18 cv ⊢ 𝑧
21 20 14 15 co ⊢ ( 𝑧 ℎ 𝑥 )
22 13 cv ⊢ 𝑓
23 20 14 cop ⊢ ⟨ 𝑧 , 𝑥 ⟩
24 cco ⊢ comp
25 4 24 cfv ⊢ ( comp ‘ 𝑐 )
26 23 16 25 co ⊢ ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 )
27 19 cv ⊢ 𝑔
28 22 27 26 co ⊢ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 )
29 19 21 28 cmpt ⊢ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) )
30 29 ccnv ⊢ ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) )
31 30 wfun ⊢ Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) )
32 31 18 11 wral ⊢ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) )
33 32 13 17 crab ⊢ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) }
34 10 12 11 11 33 cmpo ⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } )
35 9 8 34 csb ⊢ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } )
36 6 5 35 csb ⊢ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } )
37 1 2 36 cmpt ⊢ ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) )
38 0 37 wceq ⊢ Mono = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ { 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝑏 Fun ◡ ( 𝑔 ∈ ( 𝑧 ℎ 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) )