Theorem madecut

Description: Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	madecut	Could not format assertion : No typesetting found for |- ( ( ( A e. On /\ L < ( L |s R ) e. ( _Made ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simplr	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to L{\ll }_{s}R$$
2		ssltex1	$$⊢L{\ll }_{s}R\to L\in \mathrm{V}$$
3	1 2	syl	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to L\in \mathrm{V}$$
4		simprl	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to L\subseteq \mathrm{Old}\left(A\right)$$
5	3 4	elpwd	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to L\in 𝒫\mathrm{Old}\left(A\right)$$
6		ssltex2	$$⊢L{\ll }_{s}R\to R\in \mathrm{V}$$
7	1 6	syl	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to R\in \mathrm{V}$$
8		simprr	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to R\subseteq \mathrm{Old}\left(A\right)$$
9	7 8	elpwd	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to R\in 𝒫\mathrm{Old}\left(A\right)$$
10		eqidd	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to L{|}_{s}R=L{|}_{s}R$$
11		breq1	$$⊢l=L\to \left(l{\ll }_{s}r\leftrightarrow L{\ll }_{s}r\right)$$
12		oveq1	$$⊢l=L\to l{|}_{s}r=L{|}_{s}r$$
13	12	eqeq1d	$$⊢l=L\to \left(l{|}_{s}r=L{|}_{s}R\leftrightarrow L{|}_{s}r=L{|}_{s}R\right)$$
14	11 13	anbi12d	$$⊢l=L\to \left(\left(l{\ll }_{s}r\wedge l{|}_{s}r=L{|}_{s}R\right)\leftrightarrow \left(L{\ll }_{s}r\wedge L{|}_{s}r=L{|}_{s}R\right)\right)$$
15		breq2	$$⊢r=R\to \left(L{\ll }_{s}r\leftrightarrow L{\ll }_{s}R\right)$$
16		oveq2	$$⊢r=R\to L{|}_{s}r=L{|}_{s}R$$
17	16	eqeq1d	$$⊢r=R\to \left(L{|}_{s}r=L{|}_{s}R\leftrightarrow L{|}_{s}R=L{|}_{s}R\right)$$
18	15 17	anbi12d	$$⊢r=R\to \left(\left(L{\ll }_{s}r\wedge L{|}_{s}r=L{|}_{s}R\right)\leftrightarrow \left(L{\ll }_{s}R\wedge L{|}_{s}R=L{|}_{s}R\right)\right)$$
19	14 18	rspc2ev	$$⊢\left(L\in 𝒫\mathrm{Old}\left(A\right)\wedge R\in 𝒫\mathrm{Old}\left(A\right)\wedge \left(L{\ll }_{s}R\wedge L{|}_{s}R=L{|}_{s}R\right)\right)\to \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=L{|}_{s}R\right)$$
20	5 9 1 10 19	syl112anc	$$⊢\left(\left(A\in \mathrm{On}\wedge L{\ll }_{s}R\right)\wedge \left(L\subseteq \mathrm{Old}\left(A\right)\wedge R\subseteq \mathrm{Old}\left(A\right)\right)\right)\to \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=L{|}_{s}R\right)$$
21		elmade2	Could not format ( A e. On -> ( ( L |s R ) e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < ( ( L |s R ) e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
22	21	ad2antrr	Could not format ( ( ( A e. On /\ L < ( ( L |s R ) e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l < ( ( L |s R ) e. ( _Made ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
23	20 22	mpbird	Could not format ( ( ( A e. On /\ L < ( L |s R ) e. ( _Made ` A ) ) : No typesetting found for |- ( ( ( A e. On /\ L < ( L |s R ) e. ( _Made ` A ) ) with typecode |-