Metamath Proof Explorer

Theorem oppcsect

Description: A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
oppcsect.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcsect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
oppcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
oppcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
oppcsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
oppcsect.t ⊢ 𝑇 = ( Sect ‘ 𝑂 )
Assertion oppcsect ( 𝜑 → ( 𝐹 ( 𝑋 𝑇 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 oppcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 oppcsect.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3 oppcsect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 oppcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 oppcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 oppcsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
7 oppcsect.t ⊢ 𝑇 = ( Sect ‘ 𝑂 )
8 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
10 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
11 1 8 2 9 10 9 oppcco ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐶 ∈ Cat )
13 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
14 2 13 oppcid ⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
15 12 14 syl ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
16 15 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
17 11 16 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ↔ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
18 17 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ↔ ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
19 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) )
20 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21 20 2 oppchom ⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) = ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 )
22 21 eleq2i ⊢ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ↔ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
23 20 2 oppchom ⊢ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 )
24 23 eleq2i ⊢ ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ↔ 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
25 22 24 anbi12ci ⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) ↔ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) )
26 25 anbi1i ⊢ ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ↔ ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) )
27 19 26 bitri ⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ↔ ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) )
28 df-3an ⊢ ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
29 18 27 28 3bitr4g ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ↔ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
30 2 1 oppcbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
31 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
32 eqid ⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
33 eqid ⊢ ( Id ‘ 𝑂 ) = ( Id ‘ 𝑂 )
34 2 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
35 3 34 syl ⊢ ( 𝜑 → 𝑂 ∈ Cat )
36 30 31 32 33 7 35 4 5 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑇 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) ) ) )
37 1 20 8 13 6 3 4 5 issect ⊢ ( 𝜑 → ( 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
38 29 36 37 3bitr4d ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑇 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑋 𝑆 𝑌 ) 𝐹 ) )