Theorem newval

Description: The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	newval	|- ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = A -> ( _M ` x ) = ( _M ` A ) )
2		fveq2	|- ( x = A -> ( _Old ` x ) = ( _Old ` A ) )
3	1 2	difeq12d	|- ( x = A -> ( ( _M ` x ) \ ( _Old ` x ) ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
4		df-new	|- _N = ( x e. On |-> ( ( _M ` x ) \ ( _Old ` x ) ) )
5		fvex	|- ( _M ` A ) e. _V
6	5	difexi	|- ( ( _M ` A ) \ ( _Old ` A ) ) e. _V
7	3 4 6	fvmpt	|- ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
8	4	fvmptndm	|- ( -. A e. On -> ( _N ` A ) = (/) )
9		df-made	|- _M = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) )
10	9	tfr1	|- _M Fn On
11	10	fndmi	|- dom _M = On
12	11	eleq2i	|- ( A e. dom _M <-> A e. On )
13		ndmfv	|- ( -. A e. dom _M -> ( _M ` A ) = (/) )
14	12 13	sylnbir	|- ( -. A e. On -> ( _M ` A ) = (/) )
15	14	difeq1d	|- ( -. A e. On -> ( ( _M ` A ) \ ( _Old ` A ) ) = ( (/) \ ( _Old ` A ) ) )
16		0dif	|- ( (/) \ ( _Old ` A ) ) = (/)
17	15 16	eqtrdi	|- ( -. A e. On -> ( ( _M ` A ) \ ( _Old ` A ) ) = (/) )
18	8 17	eqtr4d	|- ( -. A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
19	7 18	pm2.61i	|- ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) )