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

Metamath Proof Explorer

Theorem thincsect2

Description: In a thin category, F is a section of G iff G is a section of F . Example 7.25(4) of Adamek p. 108. (Contributed by Zhi Wang, 24-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		thincsect.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2		thincsect.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		thincsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		thincsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		thincsect.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
6		ancom	⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ↔ ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
7	6	a1i	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ↔ ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ) )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9	1 2 3 4 5 8	thincsect	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) )
10	1 2 4 3 5 8	thincsect	⊢ ( 𝜑 → ( 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) ) )
11	7 9 10	3bitr4d	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) )