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