Metamath Proof Explorer


Theorem oldval

Description: The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024)

Ref Expression
Assertion oldval A On Old A = M A

Proof

Step Hyp Ref Expression
1 df-made M = recs x V | s 𝒫 ran x × 𝒫 ran x
2 recsfnon recs x V | s 𝒫 ran x × 𝒫 ran x Fn On
3 fnfun recs x V | s 𝒫 ran x × 𝒫 ran x Fn On Fun recs x V | s 𝒫 ran x × 𝒫 ran x
4 2 3 ax-mp Fun recs x V | s 𝒫 ran x × 𝒫 ran x
5 funeq M = recs x V | s 𝒫 ran x × 𝒫 ran x Fun M Fun recs x V | s 𝒫 ran x × 𝒫 ran x
6 4 5 mpbiri M = recs x V | s 𝒫 ran x × 𝒫 ran x Fun M
7 1 6 ax-mp Fun M
8 funimaexg Fun M A On M A V
9 7 8 mpan A On M A V
10 9 uniexd A On M A V
11 imaeq2 x = A M x = M A
12 11 unieqd x = A M x = M A
13 df-old Old = x On M x
14 12 13 fvmptg A On M A V Old A = M A
15 10 14 mpdan A On Old A = M A