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𝑋 ) ) ) )