Theorem cutmax

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

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

Proof

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