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

Metamath Proof Explorer

Theorem oppcsect2

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 oppcsect2 ( 𝜑 → ( 𝑋 𝑇 𝑌 ) = ◡ ( 𝑋 𝑆 𝑌 ) )

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 2 1 oppcbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
9 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
10 eqid ⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
11 eqid ⊢ ( Id ‘ 𝑂 ) = ( Id ‘ 𝑂 )
12 2 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
13 3 12 syl ⊢ ( 𝜑 → 𝑂 ∈ Cat )
14 8 9 10 11 7 13 4 5 sectss ⊢ ( 𝜑 → ( 𝑋 𝑇 𝑌 ) ⊆ ( ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) × ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) )
15 relxp ⊢ Rel ( ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) × ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) )
16 relss ⊢ ( ( 𝑋 𝑇 𝑌 ) ⊆ ( ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) × ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) → ( Rel ( ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) × ( 𝑌 ( Hom ‘ 𝑂 ) 𝑋 ) ) → Rel ( 𝑋 𝑇 𝑌 ) ) )
17 14 15 16 mpisyl ⊢ ( 𝜑 → Rel ( 𝑋 𝑇 𝑌 ) )
18 relcnv ⊢ Rel ◡ ( 𝑋 𝑆 𝑌 )
19 18 a1i ⊢ ( 𝜑 → Rel ◡ ( 𝑋 𝑆 𝑌 ) )
20 1 2 3 4 5 6 7 oppcsect ⊢ ( 𝜑 → ( 𝑓 ( 𝑋 𝑇 𝑌 ) 𝑔 ↔ 𝑔 ( 𝑋 𝑆 𝑌 ) 𝑓 ) )
21 vex ⊢ 𝑓 ∈ V
22 vex ⊢ 𝑔 ∈ V
23 21 22 brcnv ⊢ ( 𝑓 ◡ ( 𝑋 𝑆 𝑌 ) 𝑔 ↔ 𝑔 ( 𝑋 𝑆 𝑌 ) 𝑓 )
24 20 23 bitr4di ⊢ ( 𝜑 → ( 𝑓 ( 𝑋 𝑇 𝑌 ) 𝑔 ↔ 𝑓 ◡ ( 𝑋 𝑆 𝑌 ) 𝑔 ) )
25 17 19 24 eqbrrdv ⊢ ( 𝜑 → ( 𝑋 𝑇 𝑌 ) = ◡ ( 𝑋 𝑆 𝑌 ) )