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	⊢ ( 𝜑 → 𝐿 ∈ ( L ‘ 𝑋 ) )
	cutminmax.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝐿 )
	cutminmax.3	⊢ ( 𝜑 → 𝑅 ∈ ( R ‘ 𝑋 ) )
	cutminmax.4	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( R ‘ 𝑋 ) 𝑅 ≤s 𝑦 )
Assertion	cutminmax	⊢ ( 𝜑 → 𝑋 = ( { 𝐿 } |s { 𝑅 } ) )

Proof

Step	Hyp	Ref	Expression
1		cutminmax.1	⊢ ( 𝜑 → 𝐿 ∈ ( L ‘ 𝑋 ) )
2		cutminmax.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝐿 )
3		cutminmax.3	⊢ ( 𝜑 → 𝑅 ∈ ( R ‘ 𝑋 ) )
4		cutminmax.4	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( R ‘ 𝑋 ) 𝑅 ≤s 𝑦 )
5		lltropt	⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
6	5	a1i	⊢ ( 𝜑 → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
7		breq2	⊢ ( 𝑦 = 𝑏 → ( 𝑅 ≤s 𝑦 ↔ 𝑅 ≤s 𝑏 ) )
8	7	cbvralvw	⊢ ( ∀ 𝑦 ∈ ( R ‘ 𝑋 ) 𝑅 ≤s 𝑦 ↔ ∀ 𝑏 ∈ ( R ‘ 𝑋 ) 𝑅 ≤s 𝑏 )
9	4 8	sylib	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( R ‘ 𝑋 ) 𝑅 ≤s 𝑏 )
10	6 3 9	cutmin	⊢ ( 𝜑 → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑋 ) |s { 𝑅 } ) )
11		elfvdm	⊢ ( 𝐿 ∈ ( L ‘ 𝑋 ) → 𝑋 ∈ dom L )
12	1 11	syl	⊢ ( 𝜑 → 𝑋 ∈ dom L )
13		leftf	⊢ L : No ⟶ 𝒫 No
14	13	fdmi	⊢ dom L = No
15	12 14	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ No )
16		lrcut	⊢ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
17	15 16	syl	⊢ ( 𝜑 → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
18	3	snssd	⊢ ( 𝜑 → { 𝑅 } ⊆ ( R ‘ 𝑋 ) )
19		sssslt2	⊢ ( ( ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) ∧ { 𝑅 } ⊆ ( R ‘ 𝑋 ) ) → ( L ‘ 𝑋 ) <<s { 𝑅 } )
20	5 18 19	sylancr	⊢ ( 𝜑 → ( L ‘ 𝑋 ) <<s { 𝑅 } )
21		breq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ≤s 𝐿 ↔ 𝑎 ≤s 𝐿 ) )
22	21	cbvralvw	⊢ ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝐿 ↔ ∀ 𝑎 ∈ ( L ‘ 𝑋 ) 𝑎 ≤s 𝐿 )
23	2 22	sylib	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( L ‘ 𝑋 ) 𝑎 ≤s 𝐿 )
24	20 1 23	cutmax	⊢ ( 𝜑 → ( ( L ‘ 𝑋 ) |s { 𝑅 } ) = ( { 𝐿 } |s { 𝑅 } ) )
25	10 17 24	3eqtr3d	⊢ ( 𝜑 → 𝑋 = ( { 𝐿 } |s { 𝑅 } ) )