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

Metamath Proof Explorer

Theorem thincinv

Description: In a thin category, F is an inverse of G iff F is a section of G . Example 7.20(7) of Adamek p. 107. (Contributed by Zhi Wang, 24-Sep-2024)

		Ref	Expression
	Hypotheses	thincsect.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
		thincsect.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
		thincsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
		thincsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
		thincsect.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
		thincinv.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	Assertion	thincinv	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		thincsect.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2		thincsect.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		thincsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		thincsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		thincsect.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
6		thincinv.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
7	1	thinccd	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8	2 6 7 3 4 5	isinv	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) ) )
9	1 2 3 4 5	thincsect2	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) )
10	9	biimpa	⊢ ( ( 𝜑 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) → 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 )
11	8 10	mpbiran3d	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) )