Metamath Proof Explorer

Theorem invfval

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

Ref Expression
Hypotheses invfval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
invfval.n ${⊢}{N}=\mathrm{Inv}\left({C}\right)$
invfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
invfval.x ${⊢}{\phi }\to {X}\in {B}$
invfval.y ${⊢}{\phi }\to {Y}\in {B}$
invfval.s ${⊢}{S}=\mathrm{Sect}\left({C}\right)$
Assertion invfval ${⊢}{\phi }\to {X}{N}{Y}=\left({X}{S}{Y}\right)\cap {\left({Y}{S}{X}\right)}^{-1}$

Proof

Step Hyp Ref Expression
1 invfval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 invfval.n ${⊢}{N}=\mathrm{Inv}\left({C}\right)$
3 invfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
4 invfval.x ${⊢}{\phi }\to {X}\in {B}$
5 invfval.y ${⊢}{\phi }\to {Y}\in {B}$
6 invfval.s ${⊢}{S}=\mathrm{Sect}\left({C}\right)$
7 1 2 3 4 4 6 invffval ${⊢}{\phi }\to {N}=\left({x}\in {B},{y}\in {B}⟼\left({x}{S}{y}\right)\cap {\left({y}{S}{x}\right)}^{-1}\right)$
8 simprl ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {x}={X}$
9 simprr ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {y}={Y}$
10 8 9 oveq12d ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {x}{S}{y}={X}{S}{Y}$
11 9 8 oveq12d ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {y}{S}{x}={Y}{S}{X}$
12 11 cnveqd ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {\left({y}{S}{x}\right)}^{-1}={\left({Y}{S}{X}\right)}^{-1}$
13 10 12 ineq12d ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to \left({x}{S}{y}\right)\cap {\left({y}{S}{x}\right)}^{-1}=\left({X}{S}{Y}\right)\cap {\left({Y}{S}{X}\right)}^{-1}$
14 ovex ${⊢}{X}{S}{Y}\in \mathrm{V}$
15 14 inex1 ${⊢}\left({X}{S}{Y}\right)\cap {\left({Y}{S}{X}\right)}^{-1}\in \mathrm{V}$
16 15 a1i ${⊢}{\phi }\to \left({X}{S}{Y}\right)\cap {\left({Y}{S}{X}\right)}^{-1}\in \mathrm{V}$
17 7 13 4 5 16 ovmpod ${⊢}{\phi }\to {X}{N}{Y}=\left({X}{S}{Y}\right)\cap {\left({Y}{S}{X}\right)}^{-1}$