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 = Base R
staffval.i ˙ = * R
staffval.f ˙ = 𝑟𝑓 R
Assertion staffval ˙ = x B ˙ x

Proof

Step Hyp Ref Expression
1 staffval.b B = Base R
2 staffval.i ˙ = * R
3 staffval.f ˙ = 𝑟𝑓 R
4 fveq2 f = R Base f = Base R
5 4 1 syl6eqr f = R Base f = B
6 fveq2 f = R * f = * R
7 6 2 syl6eqr f = R * f = ˙
8 7 fveq1d f = R x * f = ˙ x
9 5 8 mpteq12dv f = R x Base f x * f = x B ˙ x
10 df-staf 𝑟𝑓 = f V x Base f x * f
11 eqid x B ˙ x = x B ˙ x
12 fvrn0 ˙ x ran ˙
13 12 a1i x B ˙ x ran ˙
14 11 13 fmpti x B ˙ x : B ran ˙
15 1 fvexi B V
16 2 fvexi ˙ V
17 16 rnex ran ˙ V
18 p0ex V
19 17 18 unex ran ˙ V
20 fex2 x B ˙ x : B ran ˙ B V ran ˙ V x B ˙ x V
21 14 15 19 20 mp3an x B ˙ x V
22 9 10 21 fvmpt R V 𝑟𝑓 R = x B ˙ x
23 fvprc ¬ R V 𝑟𝑓 R =
24 mpt0 x ˙ x =
25 23 24 syl6eqr ¬ R V 𝑟𝑓 R = x ˙ x
26 fvprc ¬ R V Base R =
27 1 26 syl5eq ¬ R V B =
28 27 mpteq1d ¬ R V x B ˙ x = x ˙ x
29 25 28 eqtr4d ¬ R V 𝑟𝑓 R = x B ˙ x
30 22 29 pm2.61i 𝑟𝑓 R = x B ˙ x
31 3 30 eqtri ˙ = x B ˙ x