Metamath Proof Explorer

Theorem moni

Description: Property of a monomorphism. (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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
moni.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
moni.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
moni.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑋 ) )
moni.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
Assertion moni ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) ↔ 𝐺 = 𝐾 ) )

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 moni.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 moni.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
10 moni.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑋 ) )
11 moni.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
12 1 2 3 4 5 6 7 ismon2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
13 9 12 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
14 13 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
15 10 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐺 ∈ ( 𝑍 𝐻 𝑋 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝑧 = 𝑍 )
17 16 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝑧 𝐻 𝑋 ) = ( 𝑍 𝐻 𝑋 ) )
18 15 17 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐺 ∈ ( 𝑧 𝐻 𝑋 ) )
19 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
20 19 17 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐾 ∈ ( 𝑧 𝐻 𝑋 ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) → 𝐾 ∈ ( 𝑧 𝐻 𝑋 ) )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → 𝑧 = 𝑍 )
23 22 opeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ⟨ 𝑧 , 𝑋 ⟩ = ⟨ 𝑍 , 𝑋 ⟩ )
24 23 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) = ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) )
25 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → 𝐹 = 𝐹 )
26 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → 𝑔 = 𝐺 )
27 24 25 26 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) )
28 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ℎ = 𝐾 )
29 24 25 28 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) )
30 27 29 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) ↔ ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) ) )
31 26 28 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( 𝑔 = ℎ ↔ 𝐺 = 𝐾 ) )
32 30 31 imbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) ∧ ℎ = 𝐾 ) → ( ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ↔ ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) ) )
33 21 32 rspcdv ⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝑍 ) ∧ 𝑔 = 𝐺 ) → ( ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) ) )
34 18 33 rspcimdv ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) ) )
35 8 34 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) ) )
36 14 35 mpd ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) )
37 oveq2 ⊢ ( 𝐺 = 𝐾 → ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) )
38 36 37 impbid1 ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑌 ) 𝐾 ) ↔ 𝐺 = 𝐾 ) )