This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , < ) )