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

Metamath Proof Explorer

Theorem issect

Description: The property " F is a section of G ". (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 issect ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 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 1 2 3 4 5 6 7 8 sectfval ⊢ ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } )
10 9 breqd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } 𝐺 ) )
11 oveq12 ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) )
12 11 ancoms ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) )
13 12 eqeq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
14 eqid ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) }
15 13 14 brab2a ⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
16 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
17 15 16 bitr4i ⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ‘ 𝑋 ) ) } 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
18 10 17 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) ) )