ismon

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

	Ref	Expression
Hypotheses	ismon.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	ismon.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	ismon.o	⊢ · = ( comp ‘ 𝐶 )
	ismon.s	⊢ 𝑀 = ( Mono ‘ 𝐶 )
	ismon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	ismon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ismon.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	ismon	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 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		ismon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		ismon.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8	1 2 3 4 5	monfval	⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) } ) )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
11	9 10	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
12	9	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑧 𝐻 𝑥 ) = ( 𝑧 𝐻 𝑋 ) )
13	9	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ⟨ 𝑧 , 𝑥 ⟩ = ⟨ 𝑧 , 𝑋 ⟩ )
14	13 10	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) = ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) )
15	14	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) )
16	12 15	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) )
17	16	cnveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) = ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) )
18	17	funeqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) ↔ Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
19	18	ralbidv	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) ↔ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
20	11 19	rabeqbidv	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑥 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } )
21		ovex	⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
22	21	rabex	⊢ { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } ∈ V
23	22	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } ∈ V )
24	8 20 6 7 23	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } )
25	24	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } ) )
26		oveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) )
27	26	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) )
28	27	cnveqd	⊢ ( 𝑓 = 𝐹 → ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) = ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) )
29	28	funeqd	⊢ ( 𝑓 = 𝐹 → ( Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ↔ Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
30	29	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ↔ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
31	30	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∣ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) } ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
32	25 31	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ^◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) ) )

Metamath Proof Explorer

Theorem ismon

Proof