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

Proof

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