Theorem sn-suprubd

Description: suprubd without ax-mulcom , proven trivially from sn-suprcld . (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$$
	sn-suprubd.4	$$⊢\phi \to B\in A$$
Assertion	sn-suprubd	$$⊢\phi \to B\le sup\left(A,ℝ,<\right)$$

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		sn-suprubd.4	$$⊢\phi \to B\in A$$
5	1 4	sseldd	$$⊢\phi \to B\in ℝ$$
6	1 2 3	sn-suprcld	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$
7		ltso	$$⊢<\mathrm{Or}ℝ$$
8	7	a1i	$$⊢\phi \to <\mathrm{Or}ℝ$$
9	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)$$
10	8 9	supub	$$⊢\phi \to \left(B\in A\to \neg sup\left(A,ℝ,<\right)<B\right)$$
11	4 10	mpd	$$⊢\phi \to \neg sup\left(A,ℝ,<\right)<B$$
12	5 6 11	nltled	$$⊢\phi \to B\le sup\left(A,ℝ,<\right)$$