Theorem madeval2

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

	Ref	Expression
Assertion	madeval2	Could not format assertion : No typesetting found for |- ( A e. On -> ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <

Proof

Step	Hyp	Ref	Expression
1		madeval	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 |-
2		scutcl	$$⊢a{\ll }_{s}b\to a{|}_{s}b\in \mathrm{No}$$
3		eleq1	$$⊢a{|}_{s}b=x\to \left(a{|}_{s}b\in \mathrm{No}\leftrightarrow x\in \mathrm{No}\right)$$
4	3	biimpd	$$⊢a{|}_{s}b=x\to \left(a{|}_{s}b\in \mathrm{No}\to x\in \mathrm{No}\right)$$
5	2 4	mpan9	$$⊢\left(a{\ll }_{s}b\wedge a{|}_{s}b=x\right)\to x\in \mathrm{No}$$
6	5	rexlimivw	Could not format ( E. b e. ~P U. ( _Made " A ) ( a < x e. No ) : No typesetting found for |- ( E. b e. ~P U. ( _Made " A ) ( a < x e. No ) with typecode |-
7	6	rexlimivw	Could not format ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < x e. No ) : No typesetting found for |- ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < x e. No ) with typecode |-
8	7	pm4.71ri	Could not format ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < ( x e. No /\ E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < ( x e. No /\ E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
9	8	abbii	Could not format { x | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
10		eleq1	$$⊢y=⟨a,b⟩\to \left(y\in {\ll }_s\leftrightarrow ⟨a,b⟩\in {\ll }_s\right)$$
11		breq1	$$⊢y=⟨a,b⟩\to \left(y{|}_{s}x\leftrightarrow ⟨a,b⟩{|}_{s}x\right)$$
12	10 11	anbi12d	$$⊢y=⟨a,b⟩\to \left(\left(y\in {\ll }_s\wedge y{|}_{s}x\right)\leftrightarrow \left(⟨a,b⟩\in {\ll }_s\wedge ⟨a,b⟩{|}_{s}x\right)\right)$$
13	12	rexxp	Could not format ( E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. < E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( <. a , b >. e. <. |s x ) ) : No typesetting found for |- ( E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. < E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( <. a , b >. e. <. |s x ) ) with typecode |-
14		imaindm	Could not format ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) = ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i dom |s ) ) : No typesetting found for |- ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) = ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i dom |s ) ) with typecode |-
15		dmscut	$$⊢\mathrm{dom}{|}_s={\ll }_s$$
16	15	ineq2i	Could not format ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i dom |s ) = ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i <
17	16	imaeq2i	Could not format ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i dom |s ) ) = ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i <
18	14 17	eqtri	Could not format ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) = ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i <
19	18	eleq2i	Could not format ( x e. ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) <-> x e. ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < x e. ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i <
20		vex	$$⊢x\in \mathrm{V}$$
21	20	elima	Could not format ( x e. ( |s " ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < E. y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < E. y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i <
22		elin	Could not format ( y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ y e. < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ y e. <
23	22	anbi1i	Could not format ( ( y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < ( ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ y e. < ( ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ y e. <
24		anass	Could not format ( ( ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ y e. < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ ( y e. < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ ( y e. <
25	23 24	bitri	Could not format ( ( y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ ( y e. < ( y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) /\ ( y e. <
26	25	rexbii2	Could not format ( E. y e. ( ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) i^i < E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. < E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. <
27	19 21 26	3bitri	Could not format ( x e. ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) <-> E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. < E. y e. ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ( y e. <
28		df-br	$$⊢a{\ll }_{s}b\leftrightarrow ⟨a,b⟩\in {\ll }_s$$
29	28	anbi1i	$$⊢\left(a{\ll }_{s}b\wedge a{|}_{s}b=x\right)\leftrightarrow \left(⟨a,b⟩\in {\ll }_s\wedge a{|}_{s}b=x\right)$$
30		df-ov	$$⊢a{|}_{s}b={|}_s\left(⟨a,b⟩\right)$$
31	30	eqeq1i	$$⊢a{|}_{s}b=x\leftrightarrow {|}_s\left(⟨a,b⟩\right)=x$$
32		scutf	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}$$
33		ffn	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}\to {|}_{s}Fn{\ll }_s$$
34	32 33	ax-mp	$$⊢{|}_{s}Fn{\ll }_s$$
35		fnbrfvb	$$⊢\left({|}_{s}Fn{\ll }_s\wedge ⟨a,b⟩\in {\ll }_s\right)\to \left({|}_s\left(⟨a,b⟩\right)=x\leftrightarrow ⟨a,b⟩{|}_{s}x\right)$$
36	34 35	mpan	$$⊢⟨a,b⟩\in {\ll }_s\to \left({|}_s\left(⟨a,b⟩\right)=x\leftrightarrow ⟨a,b⟩{|}_{s}x\right)$$
37	31 36	bitrid	$$⊢⟨a,b⟩\in {\ll }_s\to \left(a{|}_{s}b=x\leftrightarrow ⟨a,b⟩{|}_{s}x\right)$$
38	37	pm5.32i	$$⊢\left(⟨a,b⟩\in {\ll }_s\wedge a{|}_{s}b=x\right)\leftrightarrow \left(⟨a,b⟩\in {\ll }_s\wedge ⟨a,b⟩{|}_{s}x\right)$$
39	29 38	bitri	$$⊢\left(a{\ll }_{s}b\wedge a{|}_{s}b=x\right)\leftrightarrow \left(⟨a,b⟩\in {\ll }_s\wedge ⟨a,b⟩{|}_{s}x\right)$$
40	39	2rexbii	Could not format ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( <. a , b >. e. <. |s x ) ) : No typesetting found for |- ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( <. a , b >. e. <. |s x ) ) with typecode |-
41	13 27 40	3bitr4i	Could not format ( x e. ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) <-> E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
42	41	eqabi	Could not format ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) = { x | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
43		df-rab	Could not format { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
44	9 42 43	3eqtr4i	Could not format ( |s " ( ~P U. ( _Made " A ) X. ~P U. ( _Made " A ) ) ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
45	1 44	eqtrdi	Could not format ( A e. On -> ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <