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

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 ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) } ) )