Theorem cutmin

Description: If B has a minimum, then the minimum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Hypotheses	cutmin.1	|- ( ph -> A <
	cutmin.2	|- ( ph -> X e. B )
	cutmin.3	|- ( ph -> A. y e. B X <_s y )
Assertion	cutmin	|- ( ph -> ( A |s B ) = ( A |s { X } ) )

Proof

Step	Hyp	Ref	Expression
1		cutmin.1	|- ( ph -> A <
2		cutmin.2	|- ( ph -> X e. B )
3		cutmin.3	|- ( ph -> A. y e. B X <_s y )
4		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
5		ssltss1	|- ( A < A C_ No )
6	1 5	syl	|- ( ph -> A C_ No )
7	6	sselda	|- ( ( ph /\ x e. A ) -> x e. No )
8		slerflex	|- ( x e. No -> x <_s x )
9	7 8	syl	|- ( ( ph /\ x e. A ) -> x <_s x )
10		breq2	|- ( y = x -> ( x <_s y <-> x <_s x ) )
11	10	rspcev	|- ( ( x e. A /\ x <_s x ) -> E. y e. A x <_s y )
12	4 9 11	syl2anc	|- ( ( ph /\ x e. A ) -> E. y e. A x <_s y )
13	12	ralrimiva	|- ( ph -> A. x e. A E. y e. A x <_s y )
14		breq1	|- ( x = X -> ( x <_s y <-> X <_s y ) )
15	14	rexsng	|- ( X e. B -> ( E. x e. { X } x <_s y <-> X <_s y ) )
16	2 15	syl	|- ( ph -> ( E. x e. { X } x <_s y <-> X <_s y ) )
17	16	ralbidv	|- ( ph -> ( A. y e. B E. x e. { X } x <_s y <-> A. y e. B X <_s y ) )
18	3 17	mpbird	|- ( ph -> A. y e. B E. x e. { X } x <_s y )
19		scutcut	|- ( A < ( ( A |s B ) e. No /\ A <
20	1 19	syl	|- ( ph -> ( ( A |s B ) e. No /\ A <
21	20	simp2d	|- ( ph -> A <
22	20	simp3d	|- ( ph -> { ( A |s B ) } <
23	2	snssd	|- ( ph -> { X } C_ B )
24		sssslt2	|- ( ( { ( A |s B ) } < { ( A |s B ) } <
25	22 23 24	syl2anc	|- ( ph -> { ( A |s B ) } <
26	1 13 18 21 25	cofcut1d	|- ( ph -> ( A |s B ) = ( A |s { X } ) )