Metamath Proof Explorer


Theorem sn-sup2

Description: sup2 with exactly the same proof except for using sn-ltp1 instead of ltp1 , saving ax-mulcom . (Contributed by SN, 26-Jun-2024)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 peano2re
 |-  ( x e. RR -> ( x + 1 ) e. RR )
2 1 adantr
 |-  ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( x + 1 ) e. RR )
3 2 a1i
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( x + 1 ) e. RR ) )
4 ssel
 |-  ( A C_ RR -> ( y e. A -> y e. RR ) )
5 sn-ltp1
 |-  ( x e. RR -> x < ( x + 1 ) )
6 1 ancli
 |-  ( x e. RR -> ( x e. RR /\ ( x + 1 ) e. RR ) )
7 lttr
 |-  ( ( y e. RR /\ x e. RR /\ ( x + 1 ) e. RR ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
8 7 3expb
 |-  ( ( y e. RR /\ ( x e. RR /\ ( x + 1 ) e. RR ) ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
9 6 8 sylan2
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x /\ x < ( x + 1 ) ) -> y < ( x + 1 ) ) )
10 5 9 sylan2i
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x /\ x e. RR ) -> y < ( x + 1 ) ) )
11 10 exp4b
 |-  ( y e. RR -> ( x e. RR -> ( y < x -> ( x e. RR -> y < ( x + 1 ) ) ) ) )
12 11 com34
 |-  ( y e. RR -> ( x e. RR -> ( x e. RR -> ( y < x -> y < ( x + 1 ) ) ) ) )
13 12 pm2.43d
 |-  ( y e. RR -> ( x e. RR -> ( y < x -> y < ( x + 1 ) ) ) )
14 13 imp
 |-  ( ( y e. RR /\ x e. RR ) -> ( y < x -> y < ( x + 1 ) ) )
15 breq1
 |-  ( y = x -> ( y < ( x + 1 ) <-> x < ( x + 1 ) ) )
16 5 15 syl5ibrcom
 |-  ( x e. RR -> ( y = x -> y < ( x + 1 ) ) )
17 16 adantl
 |-  ( ( y e. RR /\ x e. RR ) -> ( y = x -> y < ( x + 1 ) ) )
18 14 17 jaod
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) )
19 18 ex
 |-  ( y e. RR -> ( x e. RR -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) )
20 4 19 syl6
 |-  ( A C_ RR -> ( y e. A -> ( x e. RR -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) ) )
21 20 com23
 |-  ( A C_ RR -> ( x e. RR -> ( y e. A -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) ) )
22 21 imp
 |-  ( ( A C_ RR /\ x e. RR ) -> ( y e. A -> ( ( y < x \/ y = x ) -> y < ( x + 1 ) ) ) )
23 22 a2d
 |-  ( ( A C_ RR /\ x e. RR ) -> ( ( y e. A -> ( y < x \/ y = x ) ) -> ( y e. A -> y < ( x + 1 ) ) ) )
24 23 ralimdv2
 |-  ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A ( y < x \/ y = x ) -> A. y e. A y < ( x + 1 ) ) )
25 24 expimpd
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> A. y e. A y < ( x + 1 ) ) )
26 3 25 jcad
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) ) )
27 ovex
 |-  ( x + 1 ) e. _V
28 eleq1
 |-  ( z = ( x + 1 ) -> ( z e. RR <-> ( x + 1 ) e. RR ) )
29 breq2
 |-  ( z = ( x + 1 ) -> ( y < z <-> y < ( x + 1 ) ) )
30 29 ralbidv
 |-  ( z = ( x + 1 ) -> ( A. y e. A y < z <-> A. y e. A y < ( x + 1 ) ) )
31 28 30 anbi12d
 |-  ( z = ( x + 1 ) -> ( ( z e. RR /\ A. y e. A y < z ) <-> ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) ) )
32 27 31 spcev
 |-  ( ( ( x + 1 ) e. RR /\ A. y e. A y < ( x + 1 ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) )
33 26 32 syl6
 |-  ( A C_ RR -> ( ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) ) )
34 33 exlimdv
 |-  ( A C_ RR -> ( E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. z ( z e. RR /\ A. y e. A y < z ) ) )
35 eleq1
 |-  ( z = x -> ( z e. RR <-> x e. RR ) )
36 breq2
 |-  ( z = x -> ( y < z <-> y < x ) )
37 36 ralbidv
 |-  ( z = x -> ( A. y e. A y < z <-> A. y e. A y < x ) )
38 35 37 anbi12d
 |-  ( z = x -> ( ( z e. RR /\ A. y e. A y < z ) <-> ( x e. RR /\ A. y e. A y < x ) ) )
39 38 cbvexvw
 |-  ( E. z ( z e. RR /\ A. y e. A y < z ) <-> E. x ( x e. RR /\ A. y e. A y < x ) )
40 34 39 syl6ib
 |-  ( A C_ RR -> ( E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) -> E. x ( x e. RR /\ A. y e. A y < x ) ) )
41 df-rex
 |-  ( E. x e. RR A. y e. A ( y < x \/ y = x ) <-> E. x ( x e. RR /\ A. y e. A ( y < x \/ y = x ) ) )
42 df-rex
 |-  ( E. x e. RR A. y e. A y < x <-> E. x ( x e. RR /\ A. y e. A y < x ) )
43 40 41 42 3imtr4g
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A ( y < x \/ y = x ) -> E. x e. RR A. y e. A y < x ) )
44 43 adantr
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A ( y < x \/ y = x ) -> E. x e. RR A. y e. A y < x ) )
45 44 imdistani
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y < x ) )
46 df-3an
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) <-> ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
47 df-3an
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) <-> ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y < x ) )
48 45 46 47 3imtr4i
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) )
49 axsup
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
50 48 49 syl
 |-  ( ( 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 ) ) )