Metamath Proof Explorer


Theorem staffval

Description: The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses staffval.b B=BaseR
staffval.i ˙=*R
staffval.f ˙=𝑟𝑓R
Assertion staffval ˙=xB˙x

Proof

Step Hyp Ref Expression
1 staffval.b B=BaseR
2 staffval.i ˙=*R
3 staffval.f ˙=𝑟𝑓R
4 fveq2 f=RBasef=BaseR
5 4 1 eqtr4di f=RBasef=B
6 fveq2 f=R*f=*R
7 6 2 eqtr4di f=R*f=˙
8 7 fveq1d f=Rx*f=˙x
9 5 8 mpteq12dv f=RxBasefx*f=xB˙x
10 df-staf 𝑟𝑓=fVxBasefx*f
11 eqid xB˙x=xB˙x
12 fvrn0 ˙xran˙
13 12 a1i xB˙xran˙
14 11 13 fmpti xB˙x:Bran˙
15 1 fvexi BV
16 2 fvexi ˙V
17 16 rnex ran˙V
18 p0ex V
19 17 18 unex ran˙V
20 fex2 xB˙x:Bran˙BVran˙VxB˙xV
21 14 15 19 20 mp3an xB˙xV
22 9 10 21 fvmpt RV𝑟𝑓R=xB˙x
23 fvprc ¬RV𝑟𝑓R=
24 mpt0 x˙x=
25 23 24 eqtr4di ¬RV𝑟𝑓R=x˙x
26 fvprc ¬RVBaseR=
27 1 26 eqtrid ¬RVB=
28 27 mpteq1d ¬RVxB˙x=x˙x
29 25 28 eqtr4d ¬RV𝑟𝑓R=xB˙x
30 22 29 pm2.61i 𝑟𝑓R=xB˙x
31 3 30 eqtri ˙=xB˙x