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	Could not format assertion : No typesetting found for |- ( A e. On -> ( X e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <

Proof

Step	Hyp	Ref	Expression
1		elmade	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 <
2		oldval	Could not format ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-
3	2	pweqd	Could not format ( A e. On -> ~P ( _Old ` A ) = ~P U. ( _Made " A ) ) : No typesetting found for |- ( A e. On -> ~P ( _Old ` A ) = ~P U. ( _Made " A ) ) with typecode |-
4	3	rexeqdv	Could not format ( A e. On -> ( E. r e. ~P ( _Old ` A ) ( l < E. r e. ~P U. ( _Made " A ) ( l < ( E. r e. ~P ( _Old ` A ) ( l < E. r e. ~P U. ( _Made " A ) ( l <
5	3 4	rexeqbidv	Could not format ( A e. On -> ( E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l < ( E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < E. l e. ~P U. ( _Made " A ) E. r e. ~P U. ( _Made " A ) ( l <
6	1 5	bitr4d	Could not format ( A e. On -> ( X e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < ( X e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <