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

Metamath Proof Explorer

Theorem sectss

Description: The section relation is a relation between morphisms from X to Y and morphisms from Y to X . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
issect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
issect.o ⊢ · = ( comp ‘ 𝐶 )
issect.i ⊢ 1 = ( Id ‘ 𝐶 )
issect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
issect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
issect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
issect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion sectss ( 𝜑 → ( 𝑋 𝑆 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 issect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 issect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 issect.o ⊢ · = ( comp ‘ 𝐶 )
4 issect.i ⊢ 1 = ( Id ‘ 𝐶 )
5 issect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
6 issect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
7 issect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 issect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 1 2 3 4 5 6 7 8 sectfval ⊢ ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } )
10 opabssxp ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) )
11 9 10 eqsstrdi ⊢ ( 𝜑 → ( 𝑋 𝑆 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )