isinv

Description: Value of the inverse relation. (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$
	invfval.x	$⊢ φ \to X \in B$
	invfval.y	$⊢ φ \to Y \in B$
	invfval.s	$⊢ S = Sect (C)$
Assertion	isinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X S Y) G \land G (Y S X) F))$

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invfval.x	$⊢ φ \to X \in B$
5		invfval.y	$⊢ φ \to Y \in B$
6		invfval.s	$⊢ S = Sect (C)$
7	1 2 3 4 5 6	invfval	$⊢ φ \to X N Y = (X S Y) \cap {(Y S X)}^{-1}$
8	7	breqd	$⊢ φ \to (F (X N Y) G \leftrightarrow F ((X S Y) \cap {(Y S X)}^{-1}) G)$
9		brin	$⊢ F ((X S Y) \cap {(Y S X)}^{-1}) G \leftrightarrow (F (X S Y) G \land F {(Y S X)}^{-1} G)$
10	8 9	bitrdi	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X S Y) G \land F {(Y S X)}^{-1} G))$
11		eqid	$⊢ Hom (C) = Hom (C)$
12		eqid	$⊢ comp (C) = comp (C)$
13		eqid	$⊢ Id (C) = Id (C)$
14	1 11 12 13 6 3 5 4	sectss	$⊢ φ \to Y S X \subseteq (Y Hom (C) X) \times (X Hom (C) Y)$
15		relxp	$⊢ Rel ((Y Hom (C) X) \times (X Hom (C) Y))$
16		relss	$⊢ Y S X \subseteq (Y Hom (C) X) \times (X Hom (C) Y) \to (Rel ((Y Hom (C) X) \times (X Hom (C) Y)) \to Rel (Y S X))$
17	14 15 16	mpisyl	$⊢ φ \to Rel (Y S X)$
18		relbrcnvg	$⊢ Rel (Y S X) \to (F {(Y S X)}^{-1} G \leftrightarrow G (Y S X) F)$
19	17 18	syl	$⊢ φ \to (F {(Y S X)}^{-1} G \leftrightarrow G (Y S X) F)$
20	19	anbi2d	$⊢ φ \to ((F (X S Y) G \land F {(Y S X)}^{-1} G) \leftrightarrow (F (X S Y) G \land G (Y S X) F))$
21	10 20	bitrd	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X S Y) G \land G (Y S X) F))$

Metamath Proof Explorer