Theorem oldval

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

	Ref	Expression
Assertion	oldval	Could not format assertion : No typesetting found for |- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-made	Could not format _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) : No typesetting found for |- _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) with typecode |-
2		recsfnon	$$⊢\mathrm{recs}\left(\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)\right)Fn\mathrm{On}$$
3		fnfun	$$⊢\mathrm{recs}\left(\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)\right)Fn\mathrm{On}\to \mathrm{Fun}\mathrm{recs}\left(\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Fun}\mathrm{recs}\left(\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)\right)$$
5		funeq	Could not format ( _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> ( Fun _Made <-> Fun recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) ) ) : No typesetting found for |- ( _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> ( Fun _Made <-> Fun recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) ) ) with typecode |-
6	4 5	mpbiri	Could not format ( _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> Fun _Made ) : No typesetting found for |- ( _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> Fun _Made ) with typecode |-
7	1 6	ax-mp	Could not format Fun _Made : No typesetting found for |- Fun _Made with typecode |-
8		funimaexg	Could not format ( ( Fun _Made /\ A e. On ) -> ( _Made " A ) e. _V ) : No typesetting found for |- ( ( Fun _Made /\ A e. On ) -> ( _Made " A ) e. _V ) with typecode |-
9	7 8	mpan	Could not format ( A e. On -> ( _Made " A ) e. _V ) : No typesetting found for |- ( A e. On -> ( _Made " A ) e. _V ) with typecode |-
10	9	uniexd	Could not format ( A e. On -> U. ( _Made " A ) e. _V ) : No typesetting found for |- ( A e. On -> U. ( _Made " A ) e. _V ) with typecode |-
11		imaeq2	Could not format ( x = A -> ( _Made " x ) = ( _Made " A ) ) : No typesetting found for |- ( x = A -> ( _Made " x ) = ( _Made " A ) ) with typecode |-
12	11	unieqd	Could not format ( x = A -> U. ( _Made " x ) = U. ( _Made " A ) ) : No typesetting found for |- ( x = A -> U. ( _Made " x ) = U. ( _Made " A ) ) with typecode |-
13		df-old	Could not format _Old = ( x e. On |-> U. ( _Made " x ) ) : No typesetting found for |- _Old = ( x e. On |-> U. ( _Made " x ) ) with typecode |-
14	12 13	fvmptg	Could not format ( ( A e. On /\ U. ( _Made " A ) e. _V ) -> ( _Old ` A ) = U. ( _Made " A ) ) : No typesetting found for |- ( ( A e. On /\ U. ( _Made " A ) e. _V ) -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-
15	10 14	mpdan	Could not format ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-