Metamath Proof Explorer


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 ssltss1 ( 𝐴 <<s 𝐵𝐴 No )
6 1 5 syl ( 𝜑𝐴 No )
7 6 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥 No )
8 slerflex ( 𝑥 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 scutcut ( 𝐴 <<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 sssslt2 ( ( { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ∧ { 𝑋 } ⊆ 𝐵 ) → { ( 𝐴 |s 𝐵 ) } <<s { 𝑋 } )
25 22 23 24 syl2anc ( 𝜑 → { ( 𝐴 |s 𝐵 ) } <<s { 𝑋 } )
26 1 13 18 21 25 cofcut1d ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐴 |s { 𝑋 } ) )