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	|- ( ( ( A e. On /\ L < ( L |s R ) e. ( _M ` A ) )

Proof

Step	Hyp	Ref	Expression
1		simplr	|- ( ( ( A e. On /\ L < L <
2		ssltex1	|- ( L < L e. _V )
3	1 2	syl	|- ( ( ( A e. On /\ L < L e. _V )
4		simprl	|- ( ( ( A e. On /\ L < L C_ ( _Old ` A ) )
5	3 4	elpwd	|- ( ( ( A e. On /\ L < L e. ~P ( _Old ` A ) )
6		ssltex2	|- ( L < R e. _V )
7	1 6	syl	|- ( ( ( A e. On /\ L < R e. _V )
8		simprr	|- ( ( ( A e. On /\ L < R C_ ( _Old ` A ) )
9	7 8	elpwd	|- ( ( ( A e. On /\ L < R e. ~P ( _Old ` A ) )
10		eqidd	|- ( ( ( A e. On /\ L < ( L |s R ) = ( L |s R ) )
11		breq1	|- ( l = L -> ( l < L <
12		oveq1	|- ( l = L -> ( l |s r ) = ( L |s r ) )
13	12	eqeq1d	|- ( l = L -> ( ( l |s r ) = ( L |s R ) <-> ( L |s r ) = ( L |s R ) ) )
14	11 13	anbi12d	|- ( l = L -> ( ( l < ( L <
15		breq2	|- ( r = R -> ( L < L <
16		oveq2	|- ( r = R -> ( L |s r ) = ( L |s R ) )
17	16	eqeq1d	|- ( r = R -> ( ( L |s r ) = ( L |s R ) <-> ( L |s R ) = ( L |s R ) ) )
18	15 17	anbi12d	|- ( r = R -> ( ( L < ( L <
19	14 18	rspc2ev	|- ( ( L e. ~P ( _Old ` A ) /\ R e. ~P ( _Old ` A ) /\ ( L < E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
20	5 9 1 10 19	syl112anc	|- ( ( ( A e. On /\ L < E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
21		elmade2	|- ( A e. On -> ( ( L |s R ) e. ( _M ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
22	21	ad2antrr	|- ( ( ( A e. On /\ L < ( ( L |s R ) e. ( _M ` A ) <-> E. l e. ~P ( _Old ` A ) E. r e. ~P ( _Old ` A ) ( l <
23	20 22	mpbird	|- ( ( ( A e. On /\ L < ( L |s R ) e. ( _M ` A ) )