Theorem madeval

Description: The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

	Ref	Expression
Assertion	madeval	Could not format assertion : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( |s " ( ~P U. ( _Made " A ) X. ~P 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	1	tfr2	Could not format ( A e. On -> ( _Made ` A ) = ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _Made |` A ) ) ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _Made |` A ) ) ) with typecode |-
3		eqid	$$⊢\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)=\left(x\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}x\times 𝒫\bigcup \mathrm{ran}x\right]\right)$$
4		rneq	Could not format ( x = ( _Made |` A ) -> ran x = ran ( _Made |` A ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> ran x = ran ( _Made |` A ) ) with typecode |-
5		df-ima	Could not format ( _Made " A ) = ran ( _Made |` A ) : No typesetting found for |- ( _Made " A ) = ran ( _Made |` A ) with typecode |-
6	4 5	eqtr4di	Could not format ( x = ( _Made |` A ) -> ran x = ( _Made " A ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> ran x = ( _Made " A ) ) with typecode |-
7	6	unieqd	Could not format ( x = ( _Made |` A ) -> U. ran x = U. ( _Made " A ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> U. ran x = U. ( _Made " A ) ) with typecode |-
8	7	pweqd	Could not format ( x = ( _Made |` A ) -> ~P U. ran x = ~P U. ( _Made " A ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> ~P U. ran x = ~P U. ( _Made " A ) ) with typecode |-
9	8	sqxpeqd	Could not format ( x = ( _Made |` A ) -> ( ~P U. ran x X. ~P U. ran x ) = ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> ( ~P U. ran x X. ~P U. ran x ) = ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) with typecode |-
10	9	imaeq2d	Could not format ( x = ( _Made |` A ) -> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) : No typesetting found for |- ( x = ( _Made |` A ) -> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) with typecode |-
11	1	tfr1	Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
12		fnfun	Could not format ( _Made Fn On -> Fun _Made ) : No typesetting found for |- ( _Made Fn On -> Fun _Made ) with typecode |-
13	11 12	ax-mp	Could not format Fun _Made : No typesetting found for |- Fun _Made with typecode |-
14		resfunexg	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 |-
15	13 14	mpan	Could not format ( A e. On -> ( _Made |` A ) e. _V ) : No typesetting found for |- ( A e. On -> ( _Made |` A ) e. _V ) with typecode |-
16		scutf	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}$$
17		ffun	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}\to \mathrm{Fun}{|}_s$$
18	16 17	ax-mp	$$⊢\mathrm{Fun}{|}_s$$
19		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 |-
20	13 19	mpan	Could not format ( A e. On -> ( _Made " A ) e. _V ) : No typesetting found for |- ( A e. On -> ( _Made " A ) e. _V ) with typecode |-
21		uniexg	Could not format ( ( _Made " A ) e. _V -> U. ( _Made " A ) e. _V ) : No typesetting found for |- ( ( _Made " A ) e. _V -> U. ( _Made " A ) e. _V ) with typecode |-
22		pwexg	Could not format ( U. ( _Made " A ) e. _V -> ~P U. ( _Made " A ) e. _V ) : No typesetting found for |- ( U. ( _Made " A ) e. _V -> ~P U. ( _Made " A ) e. _V ) with typecode |-
23	20 21 22	3syl	Could not format ( A e. On -> ~P U. ( _Made " A ) e. _V ) : No typesetting found for |- ( A e. On -> ~P U. ( _Made " A ) e. _V ) with typecode |-
24	23 23	xpexd	Could not format ( A e. On -> ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) e. _V ) : No typesetting found for |- ( A e. On -> ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) e. _V ) with typecode |-
25		funimaexg	Could not format ( ( Fun |s /\ ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) e. _V ) -> ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) e. _V ) : No typesetting found for |- ( ( Fun |s /\ ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) e. _V ) -> ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) e. _V ) with typecode |-
26	18 24 25	sylancr	Could not format ( A e. On -> ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) e. _V ) : No typesetting found for |- ( A e. On -> ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) e. _V ) with typecode |-
27	3 10 15 26	fvmptd3	Could not format ( A e. On -> ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _Made |` A ) ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) : No typesetting found for |- ( A e. On -> ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _Made |` A ) ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) with typecode |-
28	2 27	eqtrd	Could not format ( A e. On -> ( _Made ` A ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) ) with typecode |-