Metamath Proof Explorer

Theorem uzwo

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005)

Ref Expression
Assertion uzwo 
|- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( h = M -> ( h <_ t <-> M <_ t ) )
2 1 ralbidv 
 |-  ( h = M -> ( A. t e. S h <_ t <-> A. t e. S M <_ t ) )
3 2 imbi2d 
 |-  ( h = M -> ( ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S h <_ t ) <-> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S M <_ t ) ) )
4 breq1 
 |-  ( h = m -> ( h <_ t <-> m <_ t ) )
5 4 ralbidv 
 |-  ( h = m -> ( A. t e. S h <_ t <-> A. t e. S m <_ t ) )
6 5 imbi2d 
 |-  ( h = m -> ( ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S h <_ t ) <-> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S m <_ t ) ) )
7 breq1 
 |-  ( h = ( m + 1 ) -> ( h <_ t <-> ( m + 1 ) <_ t ) )
8 7 ralbidv 
 |-  ( h = ( m + 1 ) -> ( A. t e. S h <_ t <-> A. t e. S ( m + 1 ) <_ t ) )
9 8 imbi2d 
 |-  ( h = ( m + 1 ) -> ( ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S h <_ t ) <-> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S ( m + 1 ) <_ t ) ) )
10 breq1 
 |-  ( h = n -> ( h <_ t <-> n <_ t ) )
11 10 ralbidv 
 |-  ( h = n -> ( A. t e. S h <_ t <-> A. t e. S n <_ t ) )
12 11 imbi2d 
 |-  ( h = n -> ( ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S h <_ t ) <-> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S n <_ t ) ) )
13 ssel 
 |-  ( S C_ ( ZZ>= ` M ) -> ( t e. S -> t e. ( ZZ>= ` M ) ) )
14 eluzle 
 |-  ( t e. ( ZZ>= ` M ) -> M <_ t )
15 13 14 syl6 
 |-  ( S C_ ( ZZ>= ` M ) -> ( t e. S -> M <_ t ) )
16 15 ralrimiv 
 |-  ( S C_ ( ZZ>= ` M ) -> A. t e. S M <_ t )
17 16 adantr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S M <_ t )
18 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
19 sstr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ ZZ ) -> S C_ ZZ )
20 18 19 mpan2 
 |-  ( S C_ ( ZZ>= ` M ) -> S C_ ZZ )
21 eluzelz 
 |-  ( m e. ( ZZ>= ` M ) -> m e. ZZ )
22 breq1 
 |-  ( j = m -> ( j <_ t <-> m <_ t ) )
23 22 ralbidv 
 |-  ( j = m -> ( A. t e. S j <_ t <-> A. t e. S m <_ t ) )
24 23 rspcev 
 |-  ( ( m e. S /\ A. t e. S m <_ t ) -> E. j e. S A. t e. S j <_ t )
25 24 expcom 
 |-  ( A. t e. S m <_ t -> ( m e. S -> E. j e. S A. t e. S j <_ t ) )
26 25 con3rr3 
 |-  ( -. E. j e. S A. t e. S j <_ t -> ( A. t e. S m <_ t -> -. m e. S ) )
27 ssel2 
 |-  ( ( S C_ ZZ /\ t e. S ) -> t e. ZZ )
28 zre 
 |-  ( m e. ZZ -> m e. RR )
29 zre 
 |-  ( t e. ZZ -> t e. RR )
30 letri3 
 |-  ( ( m e. RR /\ t e. RR ) -> ( m = t <-> ( m <_ t /\ t <_ m ) ) )
31 28 29 30 syl2an 
 |-  ( ( m e. ZZ /\ t e. ZZ ) -> ( m = t <-> ( m <_ t /\ t <_ m ) ) )
32 zleltp1 
 |-  ( ( t e. ZZ /\ m e. ZZ ) -> ( t <_ m <-> t < ( m + 1 ) ) )
33 peano2re 
 |-  ( m e. RR -> ( m + 1 ) e. RR )
34 28 33 syl 
 |-  ( m e. ZZ -> ( m + 1 ) e. RR )
35 ltnle 
 |-  ( ( t e. RR /\ ( m + 1 ) e. RR ) -> ( t < ( m + 1 ) <-> -. ( m + 1 ) <_ t ) )
36 29 34 35 syl2an 
 |-  ( ( t e. ZZ /\ m e. ZZ ) -> ( t < ( m + 1 ) <-> -. ( m + 1 ) <_ t ) )
37 32 36 bitrd 
 |-  ( ( t e. ZZ /\ m e. ZZ ) -> ( t <_ m <-> -. ( m + 1 ) <_ t ) )
38 37 ancoms 
 |-  ( ( m e. ZZ /\ t e. ZZ ) -> ( t <_ m <-> -. ( m + 1 ) <_ t ) )
39 38 anbi2d 
 |-  ( ( m e. ZZ /\ t e. ZZ ) -> ( ( m <_ t /\ t <_ m ) <-> ( m <_ t /\ -. ( m + 1 ) <_ t ) ) )
40 31 39 bitrd 
 |-  ( ( m e. ZZ /\ t e. ZZ ) -> ( m = t <-> ( m <_ t /\ -. ( m + 1 ) <_ t ) ) )
41 27 40 sylan2 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( m = t <-> ( m <_ t /\ -. ( m + 1 ) <_ t ) ) )
42 eleq1a 
 |-  ( t e. S -> ( m = t -> m e. S ) )
43 42 ad2antll 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( m = t -> m e. S ) )
44 41 43 sylbird 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( ( m <_ t /\ -. ( m + 1 ) <_ t ) -> m e. S ) )
45 44 expd 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( m <_ t -> ( -. ( m + 1 ) <_ t -> m e. S ) ) )
46 con1 
 |-  ( ( -. ( m + 1 ) <_ t -> m e. S ) -> ( -. m e. S -> ( m + 1 ) <_ t ) )
47 45 46 syl6 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( m <_ t -> ( -. m e. S -> ( m + 1 ) <_ t ) ) )
48 47 com23 
 |-  ( ( m e. ZZ /\ ( S C_ ZZ /\ t e. S ) ) -> ( -. m e. S -> ( m <_ t -> ( m + 1 ) <_ t ) ) )
49 48 exp32 
 |-  ( m e. ZZ -> ( S C_ ZZ -> ( t e. S -> ( -. m e. S -> ( m <_ t -> ( m + 1 ) <_ t ) ) ) ) )
50 49 com34 
 |-  ( m e. ZZ -> ( S C_ ZZ -> ( -. m e. S -> ( t e. S -> ( m <_ t -> ( m + 1 ) <_ t ) ) ) ) )
51 50 imp41 
 |-  ( ( ( ( m e. ZZ /\ S C_ ZZ ) /\ -. m e. S ) /\ t e. S ) -> ( m <_ t -> ( m + 1 ) <_ t ) )
52 51 ralimdva 
 |-  ( ( ( m e. ZZ /\ S C_ ZZ ) /\ -. m e. S ) -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) )
53 52 ex 
 |-  ( ( m e. ZZ /\ S C_ ZZ ) -> ( -. m e. S -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) ) )
54 26 53 sylan9r 
 |-  ( ( ( m e. ZZ /\ S C_ ZZ ) /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S m <_ t -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) ) )
55 54 pm2.43d 
 |-  ( ( ( m e. ZZ /\ S C_ ZZ ) /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) )
56 55 expl 
 |-  ( m e. ZZ -> ( ( S C_ ZZ /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) ) )
57 21 56 syl 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( S C_ ZZ /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) ) )
58 20 57 sylani 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S m <_ t -> A. t e. S ( m + 1 ) <_ t ) ) )
59 58 a2d 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S m <_ t ) -> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S ( m + 1 ) <_ t ) ) )
60 3 6 9 12 17 59 uzind4i 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> A. t e. S n <_ t ) )
61 breq1 
 |-  ( j = n -> ( j <_ t <-> n <_ t ) )
62 61 ralbidv 
 |-  ( j = n -> ( A. t e. S j <_ t <-> A. t e. S n <_ t ) )
63 62 rspcev 
 |-  ( ( n e. S /\ A. t e. S n <_ t ) -> E. j e. S A. t e. S j <_ t )
64 63 expcom 
 |-  ( A. t e. S n <_ t -> ( n e. S -> E. j e. S A. t e. S j <_ t ) )
65 64 con3rr3 
 |-  ( -. E. j e. S A. t e. S j <_ t -> ( A. t e. S n <_ t -> -. n e. S ) )
66 65 adantl 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> ( A. t e. S n <_ t -> -. n e. S ) )
67 60 66 sylcom 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> -. n e. S ) )
68 ssel 
 |-  ( S C_ ( ZZ>= ` M ) -> ( n e. S -> n e. ( ZZ>= ` M ) ) )
69 68 con3rr3 
 |-  ( -. n e. ( ZZ>= ` M ) -> ( S C_ ( ZZ>= ` M ) -> -. n e. S ) )
70 69 adantrd 
 |-  ( -. n e. ( ZZ>= ` M ) -> ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> -. n e. S ) )
71 67 70 pm2.61i 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ -. E. j e. S A. t e. S j <_ t ) -> -. n e. S )
72 71 ex 
 |-  ( S C_ ( ZZ>= ` M ) -> ( -. E. j e. S A. t e. S j <_ t -> -. n e. S ) )
73 72 alrimdv 
 |-  ( S C_ ( ZZ>= ` M ) -> ( -. E. j e. S A. t e. S j <_ t -> A. n -. n e. S ) )
74 eq0 
 |-  ( S = (/) <-> A. n -. n e. S )
75 73 74 imbitrrdi 
 |-  ( S C_ ( ZZ>= ` M ) -> ( -. E. j e. S A. t e. S j <_ t -> S = (/) ) )
76 75 necon1ad 
 |-  ( S C_ ( ZZ>= ` M ) -> ( S =/= (/) -> E. j e. S A. t e. S j <_ t ) )
77 76 imp 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. t e. S j <_ t )
78 breq2 
 |-  ( t = k -> ( j <_ t <-> j <_ k ) )
79 78 cbvralvw 
 |-  ( A. t e. S j <_ t <-> A. k e. S j <_ k )
80 79 rexbii 
 |-  ( E. j e. S A. t e. S j <_ t <-> E. j e. S A. k e. S j <_ k )
81 77 80 sylib 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )