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

Metamath Proof Explorer

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	$⊢ B = {Base}_{C}$
		invfval.n	$⊢ N = Inv (C)$
		invfval.c	$⊢ φ \to C \in Cat$
		invss.x	$⊢ φ \to X \in B$
		invss.y	$⊢ φ \to Y \in B$
		invss.h	$⊢ H = Hom (C)$
	Assertion	invss	$⊢ φ \to X N Y \subseteq (X H Y) \times (Y H X)$

Proof

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invss.x	$⊢ φ \to X \in B$
5		invss.y	$⊢ φ \to Y \in B$
6		invss.h	$⊢ H = Hom (C)$
7		eqid	$⊢ Sect (C) = Sect (C)$
8	1 2 3 4 5 7	invfval	$⊢ φ \to X N Y = (X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}$
9		inss1	$⊢ (X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1} \subseteq X Sect (C) Y$
10	8 9	eqsstrdi	$⊢ φ \to X N Y \subseteq X Sect (C) Y$
11		eqid	$⊢ comp (C) = comp (C)$
12		eqid	$⊢ Id (C) = Id (C)$
13	1 6 11 12 7 3 4 5	sectss	$⊢ φ \to X Sect (C) Y \subseteq (X H Y) \times (Y H X)$
14	10 13	sstrd	$⊢ φ \to X N Y \subseteq (X H Y) \times (Y H X)$