Metamath Proof Explorer

Theorem invffval

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025)

		Ref	Expression
	Hypotheses	invfval.b	$⊢ B = {Base}_{C}$
		invfval.n	$⊢ N = Inv (C)$
		invfval.c	$⊢ φ \to C \in Cat$
		invffval.s	$⊢ S = Sect (C)$
	Assertion	invffval	$⊢ φ \to N = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$

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		invffval.s	$⊢ S = Sect (C)$
5		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
6	5 1	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
7		fveq2	$⊢ c = C \to Sect (c) = Sect (C)$
8	7 4	eqtr4di	$⊢ c = C \to Sect (c) = S$
9	8	oveqd	$⊢ c = C \to x Sect (c) y = x S y$
10	8	oveqd	$⊢ c = C \to y Sect (c) x = y S x$
11	10	cnveqd	$⊢ c = C \to {(y Sect (c) x)}^{-1} = {(y S x)}^{-1}$
12	9 11	ineq12d	$⊢ c = C \to (x Sect (c) y) \cap {(y Sect (c) x)}^{-1} = (x S y) \cap {(y S x)}^{-1}$
13	6 6 12	mpoeq123dv	$⊢ c = C \to (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (x Sect (c) y) \cap {(y Sect (c) x)}^{-1}) = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$
14		df-inv	$⊢ Inv = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (x Sect (c) y) \cap {(y Sect (c) x)}^{-1}))$
15	1	fvexi	$⊢ B \in V$
16	15 15	mpoex	$⊢ (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1}) \in V$
17	13 14 16	fvmpt	$⊢ C \in Cat \to Inv (C) = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$
18	3 17	syl	$⊢ φ \to Inv (C) = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$
19	2 18	eqtrid	$⊢ φ \to N = (x \in B, y \in B ⟼ (x S y) \cap {(y S x)}^{-1})$