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