Metamath Proof Explorer

Theorem idmon

Description: An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses idmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
idmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
idmon.i ⊢ 1 = ( Id ‘ 𝐶 )
idmon.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
idmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
idmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
Assertion idmon ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝑀 𝑋 ) )

Proof

Step Hyp Ref Expression
1 idmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 idmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 idmon.i ⊢ 1 = ( Id ‘ 𝐶 )
4 idmon.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 idmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 idmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
7 1 2 3 4 5 catidcl ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐶 ∈ Cat )
9 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑧 ∈ 𝐵 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
12 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) )
13 1 2 3 8 9 10 11 12 catlid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = 𝑔 )
14 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ℎ ∈ ( 𝑧 𝐻 𝑋 ) )
15 1 2 3 8 9 10 11 14 catlid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) = ℎ )
16 13 15 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ↔ 𝑔 = ℎ ) )
17 16 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) → 𝑔 = ℎ ) )
18 17 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) → 𝑔 = ℎ ) )
19 1 2 10 6 4 5 5 ismon2 ⊢ ( 𝜑 → ( ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝑀 𝑋 ) ↔ ( ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) → 𝑔 = ℎ ) ) ) )
20 7 18 19 mpbir2and ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝑀 𝑋 ) )