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	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	cutmax.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	cutmax.3	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑋 )
Assertion	cutmax	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( { 𝑋 } |s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cutmax.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		cutmax.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		cutmax.3	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑋 )
4		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑋 ) )
5	4	rexsng	⊢ ( 𝑋 ∈ 𝐴 → ( ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑋 ) )
6	2 5	syl	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑋 ) )
7	6	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑋 ) )
8	3 7	mpbird	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
10		sltsss2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
11	1 10	syl	⊢ ( 𝜑 → 𝐵 ⊆ No )
12	11	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ No )
13		lesid	⊢ ( 𝑥 ∈ No → 𝑥 ≤s 𝑥 )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ≤s 𝑥 )
15		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤s 𝑥 ↔ 𝑥 ≤s 𝑥 ) )
16	15	rspcev	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤s 𝑥 ) → ∃ 𝑦 ∈ 𝐵 𝑦 ≤s 𝑥 )
17	9 14 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 𝑦 ≤s 𝑥 )
18	17	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑦 ≤s 𝑥 )
19		cutcuts	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
20	1 19	syl	⊢ ( 𝜑 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
21	20	simp2d	⊢ ( 𝜑 → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
22	2	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐴 )
23		ssslts1	⊢ ( ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { 𝑋 } ⊆ 𝐴 ) → { 𝑋 } <<s { ( 𝐴 |s 𝐵 ) } )
24	21 22 23	syl2anc	⊢ ( 𝜑 → { 𝑋 } <<s { ( 𝐴 |s 𝐵 ) } )
25	20	simp3d	⊢ ( 𝜑 → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
26	1 8 18 24 25	cofcut1d	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( { 𝑋 } |s 𝐵 ) )