Metamath Proof Explorer


Theorem monfval

Description: Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses ismon.b 𝐵 = ( Base ‘ 𝐶 )
ismon.h 𝐻 = ( Hom ‘ 𝐶 )
ismon.o · = ( comp ‘ 𝐶 )
ismon.s 𝑀 = ( Mono ‘ 𝐶 )
ismon.c ( 𝜑𝐶 ∈ Cat )
Assertion monfval ( 𝜑𝑀 = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )

Proof

Step Hyp Ref Expression
1 ismon.b 𝐵 = ( Base ‘ 𝐶 )
2 ismon.h 𝐻 = ( Hom ‘ 𝐶 )
3 ismon.o · = ( comp ‘ 𝐶 )
4 ismon.s 𝑀 = ( Mono ‘ 𝐶 )
5 ismon.c ( 𝜑𝐶 ∈ Cat )
6 fvexd ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V )
7 fveq2 ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
8 7 1 eqtr4di ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
9 fvexd ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) ∈ V )
10 simpl ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
11 10 fveq2d ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
12 11 2 eqtr4di ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
13 simplr ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → 𝑏 = 𝐵 )
14 simpr ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → = 𝐻 )
15 14 oveqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑥 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
16 14 oveqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑧 𝑥 ) = ( 𝑧 𝐻 𝑥 ) )
17 simpll ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → 𝑐 = 𝐶 )
18 17 fveq2d ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
19 18 3 eqtr4di ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) = · )
20 19 oveqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) = ( ⟨ 𝑧 , 𝑥· 𝑦 ) )
21 20 oveqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) )
22 16 21 mpteq12dv ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) )
23 22 cnveqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) )
24 23 funeqd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) ↔ Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) ) )
25 13 24 raleqbidv ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) ↔ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) ) )
26 15 25 rabeqbidv ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → { 𝑓 ∈ ( 𝑥 𝑦 ) ∣ ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } )
27 13 13 26 mpoeq123dv ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( 𝑥𝑏 , 𝑦𝑏 ↦ { 𝑓 ∈ ( 𝑥 𝑦 ) ∣ ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )
28 9 12 27 csbied2 ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) / ( 𝑥𝑏 , 𝑦𝑏 ↦ { 𝑓 ∈ ( 𝑥 𝑦 ) ∣ ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )
29 6 8 28 csbied2 ( 𝑐 = 𝐶 ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( 𝑥𝑏 , 𝑦𝑏 ↦ { 𝑓 ∈ ( 𝑥 𝑦 ) ∣ ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )
30 df-mon Mono = ( 𝑐 ∈ Cat ↦ ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( 𝑥𝑏 , 𝑦𝑏 ↦ { 𝑓 ∈ ( 𝑥 𝑦 ) ∣ ∀ 𝑧𝑏 Fun ( 𝑔 ∈ ( 𝑧 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑦 ) 𝑔 ) ) } ) )
31 1 fvexi 𝐵 ∈ V
32 31 31 mpoex ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) ∈ V
33 29 30 32 fvmpt ( 𝐶 ∈ Cat → ( Mono ‘ 𝐶 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )
34 5 33 syl ( 𝜑 → ( Mono ‘ 𝐶 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )
35 4 34 eqtrid ( 𝜑𝑀 = ( 𝑥𝐵 , 𝑦𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥· 𝑦 ) 𝑔 ) ) } ) )