Theorem uzwo3 10960

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

Assertion

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

Distinct variable groups:   x, y, z, A   x, B, y, z

Proof of Theorem uzwo3

Dummy variable n is distinct from all other variables.

Step	Hyp	Ref	Expression
1		renegcl 9684	. . . 4 |- ( B e. RR -> -u B e. RR )
2	1	adantr 465	. . 3 |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> -u B e. RR )
3		arch 10588	. . 3 |- ( -u B e. RR -> E. n e. NN -u B < n )
4	2, 3	syl 16	. 2 |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> E. n e. NN -u B < n )
5		simplrl 759	. . . . 5 |- ( ( ( 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 759	. . . . . . . . . . . . 13 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> n e. NN )
7		nnnegz 10661	. . . . . . . . . . . . 13 |- ( n e. NN -> -u n e. ZZ )
8	6, 7	syl 16	. . . . . . . . . . . 12 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n e. ZZ )
9	8	zred 10759	. . . . . . . . . . 11 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n e. RR )
10		simprl 755	. . . . . . . . . . . 12 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. ZZ )
11	10	zred 10759	. . . . . . . . . . 11 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. RR )
12		simpll 753	. . . . . . . . . . . 12 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> B e. RR )
13	6	nnred 10349	. . . . . . . . . . . . 13 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> n e. RR )
14		simplrr 760	. . . . . . . . . . . . 13 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u B < n )
15	12, 13, 14	ltnegcon1d 9931	. . . . . . . . . . . 12 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n < B )
16		simprr 756	. . . . . . . . . . . 12 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> B <_ z )
17	9, 12, 11, 15, 16	ltletrd 9543	. . . . . . . . . . 11 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n < z )
18	9, 11, 17	ltled 9534	. . . . . . . . . 10 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> -u n <_ z )
19		eluz 10886	. . . . . . . . . . 11 |- ( ( -u n e. ZZ /\ z e. ZZ ) -> ( z e. ( ZZ>= ` -u n ) <-> -u n <_ z ) )
20	8, 10, 19	syl2anc 661	. . . . . . . . . 10 |- ( ( ( 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 232	. . . . . . . . 9 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ ( z e. ZZ /\ B <_ z ) ) -> z e. ( ZZ>= ` -u n ) )
22	21	expr 615	. . . . . . . 8 |- ( ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) /\ z e. ZZ ) -> ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
23	22	ralrimiva 2811	. . . . . . 7 |- ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) -> A. z e. ZZ ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
24		rabss 3441	. . . . . . 7 |- ( { z e. ZZ | B <_ z } C_ ( ZZ>= ` -u n ) <-> A. z e. ZZ ( B <_ z -> z e. ( ZZ>= ` -u n ) ) )
25	23, 24	sylibr 212	. . . . . 6 |- ( ( B e. RR /\ ( n e. NN /\ -u B < n ) ) -> { z e. ZZ | B <_ z } C_ ( ZZ>= ` -u n ) )
26	25	adantlr 714	. . . . 5 |- ( ( ( 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 3378	. . . 4 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A C_ ( ZZ>= ` -u n ) )
28		simplrr 760	. . . 4 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A =/= (/) )
29		infmssuzcl 10950	. . . 4 |- ( ( A C_ ( ZZ>= ` -u n ) /\ A =/= (/) ) -> sup ( A , RR , `' < ) e. A )
30	27, 28, 29	syl2anc 661	. . 3 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> sup ( A , RR , `' < ) e. A )
31		infmssuzle 10949	. . . . 5 |- ( ( A C_ ( ZZ>= ` -u n ) /\ y e. A ) -> sup ( A , RR , `' < ) <_ y )
32	27, 31	sylan 471	. . . 4 |- ( ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) /\ y e. A ) -> sup ( A , RR , `' < ) <_ y )
33	32	ralrimiva 2811	. . 3 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A. y e. A sup ( A , RR , `' < ) <_ y )
34	30	adantr 465	. . . . . . 7 |- ( ( ( ( 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 ) ) -> sup ( A , RR , `' < ) e. A )
35		simprr 756	. . . . . . 7 |- ( ( ( ( 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		breq2 4308	. . . . . . . 8 |- ( y = sup ( A , RR , `' < ) -> ( x <_ y <-> x <_ sup ( A , RR , `' < ) ) )
37	36	rspcv 3081	. . . . . . 7 |- ( sup ( A , RR , `' < ) e. A -> ( A. y e. A x <_ y -> x <_ sup ( A , RR , `' < ) ) )
38	34, 35, 37	sylc 60	. . . . . 6 |- ( ( ( ( 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 <_ sup ( A , RR , `' < ) )
39	27	adantr 465	. . . . . . 7 |- ( ( ( ( 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 ) )
40		simprl 755	. . . . . . 7 |- ( ( ( ( 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 )
41		infmssuzle 10949	. . . . . . 7 |- ( ( A C_ ( ZZ>= ` -u n ) /\ x e. A ) -> sup ( A , RR , `' < ) <_ x )
42	39, 40, 41	syl2anc 661	. . . . . 6 |- ( ( ( ( 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 ) ) -> sup ( A , RR , `' < ) <_ x )
43		uzssz 10892	. . . . . . . . . . 11 |- ( ZZ>= ` -u n ) C_ ZZ
44		zssre 10665	. . . . . . . . . . 11 |- ZZ C_ RR
45	43, 44	sstri 3377	. . . . . . . . . 10 |- ( ZZ>= ` -u n ) C_ RR
46	27, 45	syl6ss 3380	. . . . . . . . 9 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> A C_ RR )
47	46	adantr 465	. . . . . . . 8 |- ( ( ( ( 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 )
48	47, 40	sseldd 3369	. . . . . . 7 |- ( ( ( ( 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 )
49	46, 30	sseldd 3369	. . . . . . . 8 |- ( ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) /\ ( n e. NN /\ -u B < n ) ) -> sup ( A , RR , `' < ) e. RR )
50	49	adantr 465	. . . . . . 7 |- ( ( ( ( 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 ) ) -> sup ( A , RR , `' < ) e. RR )
51	48, 50	letri3d 9528	. . . . . 6 |- ( ( ( ( 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 = sup ( A , RR , `' < ) <-> ( x <_ sup ( A , RR , `' < ) /\ sup ( A , RR , `' < ) <_ x ) ) )
52	38, 42, 51	mpbir2and 913	. . . . 5 |- ( ( ( ( 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 = sup ( A , RR , `' < ) )
53	52	expr 615	. . . 4 |- ( ( ( ( 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 = sup ( A , RR , `' < ) ) )
54	53	ralrimiva 2811	. . 3 |- ( ( ( 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 = sup ( A , RR , `' < ) ) )
55		breq1 4307	. . . . 5 |- ( x = sup ( A , RR , `' < ) -> ( x <_ y <-> sup ( A , RR , `' < ) <_ y ) )
56	55	ralbidv 2747	. . . 4 |- ( x = sup ( A , RR , `' < ) -> ( A. y e. A x <_ y <-> A. y e. A sup ( A , RR , `' < ) <_ y ) )
57	56	eqreu 3163	. . 3 |- ( ( sup ( A , RR , `' < ) e. A /\ A. y e. A sup ( A , RR , `' < ) <_ y /\ A. x e. A ( A. y e. A x <_ y -> x = sup ( A , RR , `' < ) ) ) -> E! x e. A A. y e. A x <_ y )
58	30, 33, 54, 57	syl3anc 1218	. 2 |- ( ( ( 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 )
59	4, 58	rexlimddv 2857	1 |- ( ( B e. RR /\ ( A C_ { z e. ZZ | B <_ z } /\ A =/= (/) ) ) -> E! x e. A A. y e. A x <_ y )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2618   A.wral 2727   E.wrex 2728   E!wreu 2729   {crab 2731   C_ wss 3340   (/)c0 3649   class class class wbr 4304   `'ccnv 4851   ` cfv 5430   supcsup 7702   RRcr 9293   < clt 9430   <_ cle 9431   -ucneg 9608   NNcn 10334   ZZcz 10658   ZZ>=cuz 10873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371  ax-pre-sup 9372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-iun 4185  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6489  df-recs 6844  df-rdg 6878  df-er 7113  df-en 7323  df-dom 7324  df-sdom 7325  df-sup 7703  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-nn 10335  df-n0 10592  df-z 10659  df-uz 10874

This theorem is referenced by:  zmin  10961