oppcinv

Description: An inverse 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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	oppcinv.s	⊢ 𝐼 = ( Inv ‘ 𝐶 )
	oppcinv.t	⊢ 𝐽 = ( Inv ‘ 𝑂 )
Assertion	oppcinv	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( 𝑌 𝐼 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcsect.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		oppcsect.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3		oppcsect.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		oppcsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		oppcsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		oppcinv.s	⊢ 𝐼 = ( Inv ‘ 𝐶 )
7		oppcinv.t	⊢ 𝐽 = ( Inv ‘ 𝑂 )
8		incom	⊢ ( ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) ∩ ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) ) = ( ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) ∩ ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) )
9		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
10		eqid	⊢ ( Sect ‘ 𝑂 ) = ( Sect ‘ 𝑂 )
11	1 2 3 5 4 9 10	oppcsect2	⊢ ( 𝜑 → ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) = ^◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
12	11	cnveqd	⊢ ( 𝜑 → ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) = ^◡ ^◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
13		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
15		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
16	1 13 14 15 9 3 5 4	sectss	⊢ ( 𝜑 → ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ⊆ ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
17		relxp	⊢ Rel ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18		relss	⊢ ( ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ⊆ ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → ( Rel ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → Rel ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ) )
19	16 17 18	mpisyl	⊢ ( 𝜑 → Rel ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
20		dfrel2	⊢ ( Rel ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ↔ ^◡ ^◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) = ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
21	19 20	sylib	⊢ ( 𝜑 → ^◡ ^◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) = ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
22	12 21	eqtrd	⊢ ( 𝜑 → ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) = ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) )
23	1 2 3 4 5 9 10	oppcsect2	⊢ ( 𝜑 → ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) = ^◡ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) )
24	22 23	ineq12d	⊢ ( 𝜑 → ( ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) ∩ ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) ) = ( ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ∩ ^◡ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ) )
25	8 24	syl5eq	⊢ ( 𝜑 → ( ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) ∩ ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) ) = ( ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ∩ ^◡ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ) )
26	2 1	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
27	2	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
28	3 27	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
29	26 7 28 4 5 10	invfval	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( ( 𝑋 ( Sect ‘ 𝑂 ) 𝑌 ) ∩ ^◡ ( 𝑌 ( Sect ‘ 𝑂 ) 𝑋 ) ) )
30	1 6 3 5 4 9	invfval	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) = ( ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ∩ ^◡ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ) )
31	25 29 30	3eqtr4d	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( 𝑌 𝐼 𝑋 ) )

Metamath Proof Explorer

Theorem oppcinv

Proof