This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 eqtrid ⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
28 27 mpteq1d ⊢ ( ¬ 𝑅 ∈ V → ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ∗ ‘ 𝑥 ) ) )
29 25 28 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
30 22 29 pm2.61i ⊢ ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )
31 3 30 eqtri ⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )