Theorem cutpos

Description: Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	cutpos.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	cutpos.2	⊢ ( 𝜑 → 0s <s 𝐴 )
Assertion	cutpos	⊢ ( 𝜑 → 𝐴 = ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) |s ( R ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cutpos.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		cutpos.2	⊢ ( 𝜑 → 0s <s 𝐴 )
3		lltropt	⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
4	3	a1i	⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
5		lrcut	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
6	1 5	syl	⊢ ( 𝜑 → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
7	6	eqcomd	⊢ ( 𝜑 → 𝐴 = ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) )
8	1 2	0elleft	⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )
9	4 7 8	cutlt	⊢ ( 𝜑 → 𝐴 = ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) |s ( R ‘ 𝐴 ) ) )