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	|- ( ph -> A C_ RR )
	sn-sup3d.2	|- ( ph -> A =/= (/) )
	sn-sup3d.3	|- ( ph -> E. x e. RR A. y e. A y <_ x )
	sn-suprubd.4	|- ( ph -> B e. A )
Assertion	sn-suprubd	|- ( ph -> B <_ sup ( A , 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		sn-suprubd.4	|- ( ph -> B e. A )
5	1 4	sseldd	|- ( ph -> B e. RR )
6	1 2 3	sn-suprcld	|- ( ph -> sup ( A , RR , < ) e. RR )
7		ltso	|- < Or RR
8	7	a1i	|- ( ph -> < Or RR )
9	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 ) ) )
10	8 9	supub	|- ( ph -> ( B e. A -> -. sup ( A , RR , < ) < B ) )
11	4 10	mpd	|- ( ph -> -. sup ( A , RR , < ) < B )
12	5 6 11	nltled	|- ( ph -> B <_ sup ( A , RR , < ) )