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