Theorem elmade

Description: Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	elmade	Could not format assertion : No typesetting found for |- ( A e. On -> ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <

Proof

Step	Hyp	Ref	Expression
1		madef	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
2	1	ffvelcdmi	Could not format ( A e. On -> ( _Made ` A ) e. ~P No ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) e. ~P No ) with typecode |-
3	2	elpwid	Could not format ( A e. On -> ( _Made ` A ) C_ No ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) C_ No ) with typecode |-
4	3	sseld	Could not format ( A e. On -> ( X e. ( _Made ` A ) -> X e. No ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Made ` A ) -> X e. No ) ) with typecode |-
5		scutcl	$$⊢l{\ll }_{s}r\to l{|}_{s}r\in \mathrm{No}$$
6		eleq1	$$⊢l{|}_{s}r=X\to \left(l{|}_{s}r\in \mathrm{No}\leftrightarrow X\in \mathrm{No}\right)$$
7	6	biimpd	$$⊢l{|}_{s}r=X\to \left(l{|}_{s}r\in \mathrm{No}\to X\in \mathrm{No}\right)$$
8	5 7	mpan9	$$⊢\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\to X\in \mathrm{No}$$
9	8	rexlimivw	Could not format ( E. r e. ~P U. ( _Made " A ) ( l < X e. No ) : No typesetting found for |- ( E. r e. ~P U. ( _Made " A ) ( l < X e. No ) with typecode |-
10	9	rexlimivw	Could not format ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < X e. No ) : No typesetting found for |- ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < X e. No ) with typecode |-
11	10	a1i	Could not format ( A e. On -> ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < X e. No ) ) : No typesetting found for |- ( A e. On -> ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < X e. No ) ) with typecode |-
12		madeval2	Could not format ( A e. On -> ( _Made ` A ) = { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( _Made ` A ) = { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
13	12	eleq2d	Could not format ( A e. On -> ( X e. ( _Made ` A ) <-> X e. { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( X e. ( _Made ` A ) <-> X e. { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
14		eqeq2	$$⊢x=X\to \left(l{|}_{s}r=x\leftrightarrow l{|}_{s}r=X\right)$$
15	14	anbi2d	$$⊢x=X\to \left(\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$
16	15	2rexbidv	Could not format ( x = X -> ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
17	16	elrab3	Could not format ( X e. No -> ( X e. { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( X e. { x e. No | E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
18	13 17	sylan9bb	Could not format ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
19	18	ex	Could not format ( A e. On -> ( X e. No -> ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( X e. No -> ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
20	4 11 19	pm5.21ndd	Could not format ( A e. On -> ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( X e. ( _Made ` A ) <-> E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <