Theorem elmade

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

	Ref	Expression
Assertion	elmade	|- ( A e. On -> ( X e. ( _M ` A ) <-> E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <

Proof

Step	Hyp	Ref	Expression
1		madef	|- _M : On --> ~P No
2	1	ffvelrni	|- ( A e. On -> ( _M ` A ) e. ~P No )
3	2	elpwid	|- ( A e. On -> ( _M ` A ) C_ No )
4	3	sseld	|- ( A e. On -> ( X e. ( _M ` A ) -> X e. No ) )
5		scutcl	|- ( l < ( l |s r ) e. No )
6		eleq1	|- ( ( l |s r ) = X -> ( ( l |s r ) e. No <-> X e. No ) )
7	6	biimpd	|- ( ( l |s r ) = X -> ( ( l |s r ) e. No -> X e. No ) )
8	5 7	mpan9	|- ( ( l < X e. No )
9	8	rexlimivw	|- ( E. r e. ~P U. ( _M " A ) ( l < X e. No )
10	9	rexlimivw	|- ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < X e. No )
11	10	a1i	|- ( A e. On -> ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < X e. No ) )
12		madeval2	|- ( A e. On -> ( _M ` A ) = { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
13	12	eleq2d	|- ( A e. On -> ( X e. ( _M ` A ) <-> X e. { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
14		eqeq2	|- ( x = X -> ( ( l |s r ) = x <-> ( l |s r ) = X ) )
15	14	anbi2d	|- ( x = X -> ( ( l < ( l <
16	15	2rexbidv	|- ( x = X -> ( E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
17	16	elrab3	|- ( X e. No -> ( X e. { x e. No | E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l < E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
18	13 17	sylan9bb	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
19	18	ex	|- ( A e. On -> ( X e. No -> ( X e. ( _M ` A ) <-> E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
20	4 11 19	pm5.21ndd	|- ( A e. On -> ( X e. ( _M ` A ) <-> E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <