Metamath Proof Explorer


Theorem uzwo3

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 allows the lower bound B to be any real number. See also nnwo and nnwos . (Contributed by NM, 12-Nov-2004) (Proof shortened by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Assertion uzwo3
|- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> E! x e. A A. y e. A x <_ y )

Proof

Step Hyp Ref Expression
1 renegcl
 |-  ( B e. RR -> -u B e. RR )
2 1 adantr
 |-  ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> -u B e. RR )
3 arch
 |-  ( -u B e. RR -> E. n e. NN -u B < n )
4 2 3 syl
 |-  ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> E. n e. NN -u B < n )
5 simplrl
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A C_ { z e. ZZ | B <_ z } )
6 simplrl
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> n e. NN )
7 nnnegz
 |-  ( n e. NN -> -u n e. ZZ )
8 6 7 syl
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n e. ZZ )
9 8 zred
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n e. RR )
10 simprl
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. ZZ )
11 10 zred
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. RR )
12 simpll
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> B e. RR )
13 6 nnred
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> n e. RR )
14 simplrr
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u B < n )
15 12 13 14 ltnegcon1d
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n < B )
16 simprr
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> B <_ z )
17 9 12 11 15 16 ltletrd
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n < z )
18 9 11 17 ltled
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n <_ z )
19 eluz
 |-  ( ( -u n e. ZZ /\ z e. ZZ ) -> ( z e. ( ZZ>= ` -u n ) <-> -u n <_ z ) )
20 8 10 19 syl2anc
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> ( z e. ( ZZ>= ` -u n ) <-> -u n <_ z ) )
21 18 20 mpbird
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. ( ZZ>= ` -u n ) )
22 21 expr
 |-  ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ z e. ZZ ) -> ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
23 22 ralrimiva
 |-  ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) -> A. z e. ZZ ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
24 rabss
 |-  ( { z e. ZZ | B <_ z } C_ ( ZZ>= ` -u n ) <-> A. z e. ZZ ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
25 23 24 sylibr
 |-  ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) -> { z e. ZZ | B <_ z } C_ ( ZZ>= ` -u n ) )
26 25 adantlr
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> { z e. ZZ | B <_ z } C_ ( ZZ>= ` -u n ) )
27 5 26 sstrd
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A C_ ( ZZ>= ` -u n ) )
28 simplrr
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A =/= (/) )
29 infssuzcl
 |-  ( ( A C_ ( ZZ>= ` -u n ) /\ A =/= (/) ) -> inf ( A , RR , < ) e. A )
30 27 28 29 syl2anc
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> inf ( A , RR , < ) e. A )
31 infssuzle
 |-  ( ( A C_ ( ZZ>= ` -u n ) /\ y e. A ) -> inf ( A , RR , < ) <_ y )
32 27 31 sylan
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ y e. A ) -> inf ( A , RR , < ) <_ y )
33 32 ralrimiva
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A. y e. A inf ( A , RR , < ) <_ y )
34 breq2
 |-  ( y = inf ( A , RR , < ) -> ( x <_ y <-> x <_ inf ( A , RR , < ) ) )
35 simprr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> A. y e. A x <_ y )
36 30 adantr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> inf ( A , RR , < ) e. A )
37 34 35 36 rspcdva
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> x <_ inf ( A , RR , < ) )
38 27 adantr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> A C_ ( ZZ>= ` -u n ) )
39 simprl
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> x e. A )
40 infssuzle
 |-  ( ( A C_ ( ZZ>= ` -u n ) /\ x e. A ) -> inf ( A , RR , < ) <_ x )
41 38 39 40 syl2anc
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> inf ( A , RR , < ) <_ x )
42 uzssz
 |-  ( ZZ>= ` -u n ) C_ ZZ
43 zssre
 |-  ZZ C_ RR
44 42 43 sstri
 |-  ( ZZ>= ` -u n ) C_ RR
45 27 44 sstrdi
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A C_ RR )
46 45 adantr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> A C_ RR )
47 46 39 sseldd
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> x e. RR )
48 45 30 sseldd
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> inf ( A , RR , < ) e. RR )
49 48 adantr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> inf ( A , RR , < ) e. RR )
50 47 49 letri3d
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> ( x = inf ( A , RR , < ) <-> ( x <_ inf ( A , RR , < ) /\ inf ( A , RR , < ) <_ x ) ) )
51 37 41 50 mpbir2and
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ ( x e. A /\ A. y e. A x <_ y ) ) -> x = inf ( A , RR , < ) )
52 51 expr
 |-  ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ x e. A ) -> ( A. y e. A x <_ y -> x = inf ( A , RR , < ) ) )
53 52 ralrimiva
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A. x e. A ( A. y e. A x <_ y -> x = inf ( A , RR , < ) ) )
54 breq1
 |-  ( x = inf ( A , RR , < ) -> ( x <_ y <-> inf ( A , RR , < ) <_ y ) )
55 54 ralbidv
 |-  ( x = inf ( A , RR , < ) -> ( A. y e. A x <_ y <-> A. y e. A inf ( A , RR , < ) <_ y ) )
56 55 eqreu
 |-  ( ( inf ( A , RR , < ) e. A /\ A. y e. A inf ( A , RR , < ) <_ y /\ A. x e. A ( A. y e. A x <_ y -> x = inf ( A , RR , < ) ) ) -> E! x e. A A. y e. A x <_ y )
57 30 33 53 56 syl3anc
 |-  ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> E! x e. A A. y e. A x <_ y )
58 4 57 rexlimddv
 |-  ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> E! x e. A A. y e. A x <_ y )