Theorem newval

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

	Ref	Expression
Assertion	newval	Could not format assertion : No typesetting found for |- ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fveq2	Could not format ( x = A -> ( _Made ` x ) = ( _Made ` A ) ) : No typesetting found for |- ( x = A -> ( _Made ` x ) = ( _Made ` A ) ) with typecode |-
2		fveq2	$$⊢x=A\to \mathrm{Old}\left(x\right)=\mathrm{Old}\left(A\right)$$
3	1 2	difeq12d	Could not format ( x = A -> ( ( _Made ` x ) \ ( _Old ` x ) ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) : No typesetting found for |- ( x = A -> ( ( _Made ` x ) \ ( _Old ` x ) ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) with typecode |-
4		df-new	Could not format _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) : No typesetting found for |- _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) with typecode |-
5		fvex	Could not format ( _Made ` A ) e. _V : No typesetting found for |- ( _Made ` A ) e. _V with typecode |-
6	5	difexi	Could not format ( ( _Made ` A ) \ ( _Old ` A ) ) e. _V : No typesetting found for |- ( ( _Made ` A ) \ ( _Old ` A ) ) e. _V with typecode |-
7	3 4 6	fvmpt	Could not format ( A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) : No typesetting found for |- ( A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) with typecode |-
8	4	fvmptndm	Could not format ( -. A e. On -> ( _New ` A ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( _New ` A ) = (/) ) with typecode |-
9		df-made	Could not format _Made = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) ) : No typesetting found for |- _Made = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) ) with typecode |-
10	9	tfr1	Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
11	10	fndmi	Could not format dom _Made = On : No typesetting found for |- dom _Made = On with typecode |-
12	11	eleq2i	Could not format ( A e. dom _Made <-> A e. On ) : No typesetting found for |- ( A e. dom _Made <-> A e. On ) with typecode |-
13		ndmfv	Could not format ( -. A e. dom _Made -> ( _Made ` A ) = (/) ) : No typesetting found for |- ( -. A e. dom _Made -> ( _Made ` A ) = (/) ) with typecode |-
14	12 13	sylnbir	Could not format ( -. A e. On -> ( _Made ` A ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( _Made ` A ) = (/) ) with typecode |-
15	14	difeq1d	Could not format ( -. A e. On -> ( ( _Made ` A ) \ ( _Old ` A ) ) = ( (/) \ ( _Old ` A ) ) ) : No typesetting found for |- ( -. A e. On -> ( ( _Made ` A ) \ ( _Old ` A ) ) = ( (/) \ ( _Old ` A ) ) ) with typecode |-
16		0dif	$$⊢\varnothing \setminus \mathrm{Old}\left(A\right)=\varnothing$$
17	15 16	eqtrdi	Could not format ( -. A e. On -> ( ( _Made ` A ) \ ( _Old ` A ) ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( ( _Made ` A ) \ ( _Old ` A ) ) = (/) ) with typecode |-
18	8 17	eqtr4d	Could not format ( -. A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) : No typesetting found for |- ( -. A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) with typecode |-
19	7 18	pm2.61i	Could not format ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) : No typesetting found for |- ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) with typecode |-