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	$$⊢\phi \to A\in \mathrm{No}$$
	cutpos.2	No typesetting found for |- ( ph -> 0s
Assertion	cutpos	Could not format assertion : No typesetting found for |- ( ph -> A = ( ( { 0s } u. { x e. ( _Left ` A ) | 0s

Proof

Step	Hyp	Ref	Expression
1		cutpos.1	$$⊢\phi \to A\in \mathrm{No}$$
2		cutpos.2	Could not format ( ph -> 0s 0s
3		lltropt	Could not format ( _Left ` A ) <
4	3	a1i	Could not format ( ph -> ( _Left ` A ) < ( _Left ` A ) <
5		lrcut	Could not format ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
6	1 5	syl	Could not format ( ph -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( ph -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
7	6	eqcomd	Could not format ( ph -> A = ( ( _Left ` A ) |s ( _Right ` A ) ) ) : No typesetting found for |- ( ph -> A = ( ( _Left ` A ) |s ( _Right ` A ) ) ) with typecode |-
8	1 2	0elleft	Could not format ( ph -> 0s e. ( _Left ` A ) ) : No typesetting found for |- ( ph -> 0s e. ( _Left ` A ) ) with typecode |-
9	4 7 8	cutlt	Could not format ( ph -> A = ( ( { 0s } u. { x e. ( _Left ` A ) | 0s A = ( ( { 0s } u. { x e. ( _Left ` A ) | 0s