Metamath Proof Explorer

Theorem idepi

Description: An identity arrow, or an identity morphism, is an epimorphism. (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
idepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
Assertion idepi ( 𝜑 → ( 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 idepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
7 1 2 3 4 5 catidcl ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → 𝐶 ∈ Cat )
9 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → 𝑋 ∈ 𝐵 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
12 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) )
13 1 2 3 8 9 10 11 12 catrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = 𝑔 )
14 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → ℎ ∈ ( 𝑋 𝐻 𝑧 ) )
15 1 2 3 8 9 10 11 14 catrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → ( ℎ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = ℎ )
16 13 15 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = ( ℎ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) ↔ 𝑔 = ℎ ) )
17 16 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = ( ℎ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) → 𝑔 = ℎ ) )
18 17 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = ( ℎ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) → 𝑔 = ℎ ) )
19 1 2 10 6 4 5 5 isepi2 ⊢ ( 𝜑 → ( ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐸 𝑋 ) ↔ ( ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑋 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) = ( ℎ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 1 ‘ 𝑋 ) ) → 𝑔 = ℎ ) ) ) )
20 7 18 19 mpbir2and ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐸 𝑋 ) )