Theorem cutminmax

Description: If the left set of X has a maximum and the right set of X has a minimum, then X is equal to the cut of the maximum and the minimum. (Contributed by Scott Fenton, 23-Feb-2026)

	Ref	Expression
Hypotheses	cutminmax.1	|- ( ph -> L e. ( _Left ` X ) )
	cutminmax.2	|- ( ph -> A. x e. ( _Left ` X ) x <_s L )
	cutminmax.3	|- ( ph -> R e. ( _Right ` X ) )
	cutminmax.4	|- ( ph -> A. y e. ( _Right ` X ) R <_s y )
Assertion	cutminmax	|- ( ph -> X = ( { L } |s { R } ) )

Proof

Step	Hyp	Ref	Expression
1		cutminmax.1	|- ( ph -> L e. ( _Left ` X ) )
2		cutminmax.2	|- ( ph -> A. x e. ( _Left ` X ) x <_s L )
3		cutminmax.3	|- ( ph -> R e. ( _Right ` X ) )
4		cutminmax.4	|- ( ph -> A. y e. ( _Right ` X ) R <_s y )
5		lltropt	|- ( _Left ` X ) <
6	5	a1i	|- ( ph -> ( _Left ` X ) <
7		breq2	|- ( y = b -> ( R <_s y <-> R <_s b ) )
8	7	cbvralvw	|- ( A. y e. ( _Right ` X ) R <_s y <-> A. b e. ( _Right ` X ) R <_s b )
9	4 8	sylib	|- ( ph -> A. b e. ( _Right ` X ) R <_s b )
10	6 3 9	cutmin	|- ( ph -> ( ( _Left ` X ) |s ( _Right ` X ) ) = ( ( _Left ` X ) |s { R } ) )
11		elfvdm	|- ( L e. ( _Left ` X ) -> X e. dom _Left )
12	1 11	syl	|- ( ph -> X e. dom _Left )
13		leftf	|- _Left : No --> ~P No
14	13	fdmi	|- dom _Left = No
15	12 14	eleqtrdi	|- ( ph -> X e. No )
16		lrcut	|- ( X e. No -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
17	15 16	syl	|- ( ph -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
18	3	snssd	|- ( ph -> { R } C_ ( _Right ` X ) )
19		sssslt2	|- ( ( ( _Left ` X ) < ( _Left ` X ) <
20	5 18 19	sylancr	|- ( ph -> ( _Left ` X ) <
21		breq1	|- ( x = a -> ( x <_s L <-> a <_s L ) )
22	21	cbvralvw	|- ( A. x e. ( _Left ` X ) x <_s L <-> A. a e. ( _Left ` X ) a <_s L )
23	2 22	sylib	|- ( ph -> A. a e. ( _Left ` X ) a <_s L )
24	20 1 23	cutmax	|- ( ph -> ( ( _Left ` X ) |s { R } ) = ( { L } |s { R } ) )
25	10 17 24	3eqtr3d	|- ( ph -> X = ( { L } |s { R } ) )