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	$$⊢\phi \to A\subseteq ℝ$$
	sn-sup3d.2	$$⊢\phi \to A\ne \varnothing$$
	sn-sup3d.3	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
Assertion	sn-suprcld	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		sn-sup3d.1	$$⊢\phi \to A\subseteq ℝ$$
2		sn-sup3d.2	$$⊢\phi \to A\ne \varnothing$$
3		sn-sup3d.3	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
4		ltso	$$⊢<\mathrm{Or}ℝ$$
5	4	a1i	$$⊢\phi \to <\mathrm{Or}ℝ$$
6	1 2 3	sn-sup3d	$$⊢\phi \to \exists x\in ℝ\left(\forall y\in A\neg x<y\wedge \forall y\in ℝ\left(y<x\to \exists z\in Ay<z\right)\right)$$
7	5 6	supcl	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$