This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincepi

Description: In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi . (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincid.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
thincid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
Assertion thincepi ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )

Proof

Step Hyp Ref Expression
1 thincid.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 thincid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 thincmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 thincepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
7 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑌 ∈ 𝐵 )
8 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
9 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) )
10 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → ℎ ∈ ( 𝑌 𝐻 𝑧 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝐶 ∈ ThinCat )
12 7 8 9 10 2 3 11 thincmo2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑔 = ℎ )
13 12 a1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) → 𝑔 = ℎ ) )
14 13 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) → 𝑔 = ℎ ) )
15 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
16 1 thinccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
17 2 3 15 6 16 4 5 isepi2 ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) → 𝑔 = ℎ ) ) ) )
18 14 17 mpbiran2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐸 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
19 18 eqrdv ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )