Theorem staffval

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

	Ref	Expression
Hypotheses	staffval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
	staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
Assertion	staffval	⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		staffval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
3		staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
4		fveq2	⊢ ( 𝑓 = 𝑅 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑓 = 𝑅 → ( Base ‘ 𝑓 ) = 𝐵 )
6		fveq2	⊢ ( 𝑓 = 𝑅 → ( *𝑟 ‘ 𝑓 ) = ( *𝑟 ‘ 𝑅 ) )
7	6 2	eqtr4di	⊢ ( 𝑓 = 𝑅 → ( *𝑟 ‘ 𝑓 ) = ∗ )
8	7	fveq1d	⊢ ( 𝑓 = 𝑅 → ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) = ( ∗ ‘ 𝑥 ) )
9	5 8	mpteq12dv	⊢ ( 𝑓 = 𝑅 → ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
10		df-staf	⊢ *rf = ( 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑓 ) ↦ ( ( *𝑟 ‘ 𝑓 ) ‘ 𝑥 ) ) )
11		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )
12		fvrn0	⊢ ( ∗ ‘ 𝑥 ) ∈ ( ran ∗ ∪ { ∅ } )
13	12	a1i	⊢ ( 𝑥 ∈ 𝐵 → ( ∗ ‘ 𝑥 ) ∈ ( ran ∗ ∪ { ∅ } ) )
14	11 13	fmpti	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) : 𝐵 ⟶ ( ran ∗ ∪ { ∅ } )
15	1	fvexi	⊢ 𝐵 ∈ V
16	2	fvexi	⊢ ∗ ∈ V
17	16	rnex	⊢ ran ∗ ∈ V
18		p0ex	⊢ { ∅ } ∈ V
19	17 18	unex	⊢ ( ran ∗ ∪ { ∅ } ) ∈ V
20		fex2	⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) : 𝐵 ⟶ ( ran ∗ ∪ { ∅ } ) ∧ 𝐵 ∈ V ∧ ( ran ∗ ∪ { ∅ } ) ∈ V ) → ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) ∈ V )
21	14 15 19 20	mp3an	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) ∈ V
22	9 10 21	fvmpt	⊢ ( 𝑅 ∈ V → ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
23		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( *rf ‘ 𝑅 ) = ∅ )
24		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ ( ∗ ‘ 𝑥 ) ) = ∅
25	23 24	eqtr4di	⊢ ( ¬ 𝑅 ∈ V → ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ ∅ ↦ ( ∗ ‘ 𝑥 ) ) )
26		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
27	1 26	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
28	27	mpteq1d	⊢ ( ¬ 𝑅 ∈ V → ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ∗ ‘ 𝑥 ) ) )
29	25 28	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
30	22 29	pm2.61i	⊢ ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )
31	3 30	eqtri	⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )