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 )