Theorem elmade2

Description: Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elmade	|- ( A e. On -> ( X e. ( _M ` A ) <-> E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
2		oldval	|- ( A e. On -> ( _Old ` A ) = U. ( _M " A ) )
3	2	pweqd	|- ( A e. On -> ~P ( _Old ` A ) = ~P U. ( _M " A ) )
4	3	rexeqdv	|- ( A e. On -> ( E. r e. ~P ( _Old ` A ) ( l < E. r e. ~P U. ( _M " A ) ( l <
5	3 4	rexeqbidv	|- ( A e. On -> ( E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < E. l e. ~P U. ( _M " A ) E. r e. ~P U. ( _M " A ) ( l <
6	1 5	bitr4d	|- ( A e. On -> ( X e. ( _M ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <