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

Metamath Proof Explorer

Theorem issect2

Description: Property of being a section. (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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
issect.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
issect.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
Assertion issect2 ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )

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 issect.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
10 issect.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
11 9 10 jca ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) )
12 1 2 3 4 5 6 7 8 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) ) )
13 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
14 12 13 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) ) )
15 11 14 mpbirand ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )