invfval

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017)

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 6	invffval	$⊢ φ \to N = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$
8		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
9		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
10	8 9	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x S y = X S Y$
11	9 8	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to y S x = Y S X$
12	11	cnveqd	$⊢ (φ \land (x = X \land y = Y)) \to {(y S x)}^{-1} = {(Y S X)}^{-1}$
13	10 12	ineq12d	$⊢ (φ \land (x = X \land y = Y)) \to (x S y) \cap {(y S x)}^{-1} = (X S Y) \cap {(Y S X)}^{-1}$
14		ovex	$⊢ X S Y \in V$
15	14	inex1	$⊢ (X S Y) \cap {(Y S X)}^{-1} \in V$
16	15	a1i	$⊢ φ \to (X S Y) \cap {(Y S X)}^{-1} \in V$
17	7 13 4 5 16	ovmpod	$⊢ φ \to X N Y = (X S Y) \cap {(Y S X)}^{-1}$

Metamath Proof Explorer