Metamath Proof Explorer

Theorem ismon2

Description: Write out the monomorphism property directly. (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 ismon2 ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )

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 6 7 ismon ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) ) )
9 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐶 ∈ Cat )
10 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑧 ∈ 𝐵 )
11 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
12 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
13 simprr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
15 1 2 3 9 10 11 12 13 14 catcocl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) )
16 15 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ) → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) )
17 16 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) → ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) )
18 eqid ⊢ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) )
19 18 fmpt ⊢ ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) ↔ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) ⟶ ( 𝑧 𝐻 𝑌 ) )
20 df-f1 ⊢ ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) –1-1→ ( 𝑧 𝐻 𝑌 ) ↔ ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) ⟶ ( 𝑧 𝐻 𝑌 ) ∧ Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
21 20 baib ⊢ ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) ⟶ ( 𝑧 𝐻 𝑌 ) → ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) –1-1→ ( 𝑧 𝐻 𝑌 ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
22 19 21 sylbi ⊢ ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) → ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) –1-1→ ( 𝑧 𝐻 𝑌 ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) )
23 oveq2 ⊢ ( 𝑔 = ℎ → ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) )
24 18 23 f1mpt ⊢ ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) –1-1→ ( 𝑧 𝐻 𝑌 ) ↔ ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) ∧ ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
25 24 baib ⊢ ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) → ( ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) : ( 𝑧 𝐻 𝑋 ) –1-1→ ( 𝑧 𝐻 𝑌 ) ↔ ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
26 22 25 bitr3d ⊢ ( ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ∈ ( 𝑧 𝐻 𝑌 ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ↔ ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
27 17 26 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ↔ ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
28 27 ralbidva ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) )
29 28 pm5.32da ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 Fun ◡ ( 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
30 8 29 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑧 , 𝑋 ⟩ · 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )