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\in \mathrm{On}\to \left(X\in M\left(A\right)\leftrightarrow \exists l\in 𝒫\mathrm{Old}\left(A\right)\exists r\in 𝒫\mathrm{Old}\left(A\right)\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmade	$$⊢A\in \mathrm{On}\to \left(X\in M\left(A\right)\leftrightarrow \exists l\in 𝒫\bigcup M\left[A\right]\exists r\in 𝒫\bigcup M\left[A\right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$
2		oldval	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(A\right)=\bigcup M\left[A\right]$$
3	2	pweqd	$$⊢A\in \mathrm{On}\to 𝒫\mathrm{Old}\left(A\right)=𝒫\bigcup M\left[A\right]$$
4	3	rexeqdv	$$⊢A\in \mathrm{On}\to \left(\exists r\in 𝒫\mathrm{Old}\left(A\right)\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\leftrightarrow \exists r\in 𝒫\bigcup M\left[A\right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$
5	3 4	rexeqbidv	$$⊢A\in \mathrm{On}\to \left(\exists l\in 𝒫\mathrm{Old}\left(A\right)\exists r\in 𝒫\mathrm{Old}\left(A\right)\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\leftrightarrow \exists l\in 𝒫\bigcup M\left[A\right]\exists r\in 𝒫\bigcup M\left[A\right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$
6	1 5	bitr4d	$$⊢A\in \mathrm{On}\to \left(X\in M\left(A\right)\leftrightarrow \exists l\in 𝒫\mathrm{Old}\left(A\right)\exists r\in 𝒫\mathrm{Old}\left(A\right)\left(l{\ll }_{s}r\wedge l{|}_{s}r=X\right)\right)$$