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

Metamath Proof Explorer

Theorem sn-sup3d

Description: sup3 without ax-mulcom , proven trivially from sn-sup2 . (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-sup3d 
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )

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 ssel 
 |-  ( A C_ RR -> ( y e. A -> y e. RR ) )
5 leloe 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
6 5 expcom 
 |-  ( x e. RR -> ( y e. RR -> ( y <_ x <-> ( y < x \/ y = x ) ) ) )
7 4 6 syl9 
 |-  ( A C_ RR -> ( x e. RR -> ( y e. A -> ( y <_ x <-> ( y < x \/ y = x ) ) ) ) )
8 7 imp31 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
9 8 ralbidva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y <_ x <-> A. y e. A ( y < x \/ y = x ) ) )
10 9 rexbidva 
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A y <_ x <-> E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
11 1 10 syl 
 |-  ( ph -> ( E. x e. RR A. y e. A y <_ x <-> E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
12 3 11 mpbid 
 |-  ( ph -> E. x e. RR A. y e. A ( y < x \/ y = x ) )
13 sn-sup2 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
14 1 2 12 13 syl3anc 
 |-  ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )