Theorem invss

Description: The inverse relation is a relation between morphisms F : X --> Y and their inverses G : Y --> X . (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invfval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	invss.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	invss	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		invfval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		invss.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
7		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
8	1 2 3 4 5 7	invfval	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) = ( ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ∩ ◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ) )
9		inss1	⊢ ( ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ∩ ◡ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ) ⊆ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 )
10	8 9	eqsstrdi	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) ⊆ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) )
11		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
12		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
13	1 6 11 12 7 3 4 5	sectss	⊢ ( 𝜑 → ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
14	10 13	sstrd	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )