Theorem sn-suprcld

Description: suprcld without ax-mulcom , proven trivially from sn-sup3d . (Contributed by SN, 29-Jun-2025)

	Ref	Expression
Hypotheses	sn-sup3d.1	|- ( ph -> A C_ RR )
	sn-sup3d.2	|- ( ph -> A =/= (/) )
	sn-sup3d.3	|- ( ph -> E. x e. RR A. y e. A y <_ x )
Assertion	sn-suprcld	|- ( ph -> sup ( A , RR , < ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		sn-sup3d.1	|- ( ph -> A C_ RR )
2		sn-sup3d.2	|- ( ph -> A =/= (/) )
3		sn-sup3d.3	|- ( ph -> E. x e. RR A. y e. A y <_ x )
4		ltso	|- < Or RR
5	4	a1i	|- ( ph -> < Or RR )
6	1 2 3	sn-sup3d	|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
7	5 6	supcl	|- ( ph -> sup ( A , RR , < ) e. RR )