Metamath Proof Explorer

Theorem uzwo4

Description: Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses uzwo4.1 
|- F/ j ps
uzwo4.2 
|- ( j = k -> ( ph <-> ps ) )
Assertion uzwo4 
|- ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )

Proof

Step Hyp Ref Expression
1 uzwo4.1 
 |-  F/ j ps
2 uzwo4.2 
 |-  ( j = k -> ( ph <-> ps ) )
3 ssrab2 
 |-  { j e. S | ph } C_ S
4 3 a1i 
 |-  ( S C_ ( ZZ>= ` M ) -> { j e. S | ph } C_ S )
5 id 
 |-  ( S C_ ( ZZ>= ` M ) -> S C_ ( ZZ>= ` M ) )
6 4 5 sstrd 
 |-  ( S C_ ( ZZ>= ` M ) -> { j e. S | ph } C_ ( ZZ>= ` M ) )
7 6 adantr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> { j e. S | ph } C_ ( ZZ>= ` M ) )
8 rabn0 
 |-  ( { j e. S | ph } =/= (/) <-> E. j e. S ph )
9 8 bicomi 
 |-  ( E. j e. S ph <-> { j e. S | ph } =/= (/) )
10 9 biimpi 
 |-  ( E. j e. S ph -> { j e. S | ph } =/= (/) )
11 10 adantl 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> { j e. S | ph } =/= (/) )
12 uzwo 
 |-  ( ( { j e. S | ph } C_ ( ZZ>= ` M ) /\ { j e. S | ph } =/= (/) ) -> E. i e. { j e. S | ph } A. k e. { j e. S | ph } i <_ k )
13 7 11 12 syl2anc 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. i e. { j e. S | ph } A. k e. { j e. S | ph } i <_ k )
14 3 sseli 
 |-  ( i e. { j e. S | ph } -> i e. S )
15 14 adantr 
 |-  ( ( i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> i e. S )
16 15 3adant1 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> i e. S )
17 nfcv 
 |-  F/_ j i
18 nfcv 
 |-  F/_ j S
19 17 nfsbc1 
 |-  F/ j [. i / j ]. ph
20 sbceq1a 
 |-  ( j = i -> ( ph <-> [. i / j ]. ph ) )
21 17 18 19 20 elrabf 
 |-  ( i e. { j e. S | ph } <-> ( i e. S /\ [. i / j ]. ph ) )
22 21 biimpi 
 |-  ( i e. { j e. S | ph } -> ( i e. S /\ [. i / j ]. ph ) )
23 22 simprd 
 |-  ( i e. { j e. S | ph } -> [. i / j ]. ph )
24 23 adantr 
 |-  ( ( i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> [. i / j ]. ph )
25 24 3adant1 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> [. i / j ]. ph )
26 nfv 
 |-  F/ k S C_ ( ZZ>= ` M )
27 nfv 
 |-  F/ k i e. { j e. S | ph }
28 nfra1 
 |-  F/ k A. k e. { j e. S | ph } i <_ k
29 26 27 28 nf3an 
 |-  F/ k ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k )
30 simpl13 
 |-  ( ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) /\ ps ) -> A. k e. { j e. S | ph } i <_ k )
31 simpl2 
 |-  ( ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) /\ ps ) -> k e. S )
32 simpr 
 |-  ( ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) /\ ps ) -> ps )
33 simpll 
 |-  ( ( ( A. k e. { j e. S | ph } i <_ k /\ k e. S ) /\ ps ) -> A. k e. { j e. S | ph } i <_ k )
34 id 
 |-  ( ( k e. S /\ ps ) -> ( k e. S /\ ps ) )
35 nfcv 
 |-  F/_ j k
36 35 18 1 2 elrabf 
 |-  ( k e. { j e. S | ph } <-> ( k e. S /\ ps ) )
37 34 36 sylibr 
 |-  ( ( k e. S /\ ps ) -> k e. { j e. S | ph } )
38 37 adantll 
 |-  ( ( ( A. k e. { j e. S | ph } i <_ k /\ k e. S ) /\ ps ) -> k e. { j e. S | ph } )
39 rspa 
 |-  ( ( A. k e. { j e. S | ph } i <_ k /\ k e. { j e. S | ph } ) -> i <_ k )
40 33 38 39 syl2anc 
 |-  ( ( ( A. k e. { j e. S | ph } i <_ k /\ k e. S ) /\ ps ) -> i <_ k )
41 30 31 32 40 syl21anc 
 |-  ( ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) /\ ps ) -> i <_ k )
42 6 sselda 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } ) -> i e. ( ZZ>= ` M ) )
43 eluzelz 
 |-  ( i e. ( ZZ>= ` M ) -> i e. ZZ )
44 42 43 syl 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } ) -> i e. ZZ )
45 44 zred 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } ) -> i e. RR )
46 45 3adant3 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> i e. RR )
47 46 3ad2ant1 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) -> i e. RR )
48 ssel2 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ k e. S ) -> k e. ( ZZ>= ` M ) )
49 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
50 48 49 syl 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ k e. S ) -> k e. ZZ )
51 50 zred 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ k e. S ) -> k e. RR )
52 51 3ad2antl1 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S ) -> k e. RR )
53 52 3adant3 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) -> k e. RR )
54 simp3 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) -> k < i )
55 simp3 
 |-  ( ( i e. RR /\ k e. RR /\ k < i ) -> k < i )
56 simp2 
 |-  ( ( i e. RR /\ k e. RR /\ k < i ) -> k e. RR )
57 simp1 
 |-  ( ( i e. RR /\ k e. RR /\ k < i ) -> i e. RR )
58 56 57 ltnled 
 |-  ( ( i e. RR /\ k e. RR /\ k < i ) -> ( k < i <-> -. i <_ k ) )
59 55 58 mpbid 
 |-  ( ( i e. RR /\ k e. RR /\ k < i ) -> -. i <_ k )
60 47 53 54 59 syl3anc 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) -> -. i <_ k )
61 60 adantr 
 |-  ( ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) /\ ps ) -> -. i <_ k )
62 41 61 pm2.65da 
 |-  ( ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) /\ k e. S /\ k < i ) -> -. ps )
63 62 3exp 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> ( k e. S -> ( k < i -> -. ps ) ) )
64 29 63 ralrimi 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> A. k e. S ( k < i -> -. ps ) )
65 25 64 jca 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> ( [. i / j ]. ph /\ A. k e. S ( k < i -> -. ps ) ) )
66 nfv 
 |-  F/ j k < i
67 1 nfn 
 |-  F/ j -. ps
68 66 67 nfim 
 |-  F/ j ( k < i -> -. ps )
69 18 68 nfralw 
 |-  F/ j A. k e. S ( k < i -> -. ps )
70 19 69 nfan 
 |-  F/ j ( [. i / j ]. ph /\ A. k e. S ( k < i -> -. ps ) )
71 breq2 
 |-  ( j = i -> ( k < j <-> k < i ) )
72 71 imbi1d 
 |-  ( j = i -> ( ( k < j -> -. ps ) <-> ( k < i -> -. ps ) ) )
73 72 ralbidv 
 |-  ( j = i -> ( A. k e. S ( k < j -> -. ps ) <-> A. k e. S ( k < i -> -. ps ) ) )
74 20 73 anbi12d 
 |-  ( j = i -> ( ( ph /\ A. k e. S ( k < j -> -. ps ) ) <-> ( [. i / j ]. ph /\ A. k e. S ( k < i -> -. ps ) ) ) )
75 70 74 rspce 
 |-  ( ( i e. S /\ ( [. i / j ]. ph /\ A. k e. S ( k < i -> -. ps ) ) ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )
76 16 65 75 syl2anc 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ i e. { j e. S | ph } /\ A. k e. { j e. S | ph } i <_ k ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )
77 76 3exp 
 |-  ( S C_ ( ZZ>= ` M ) -> ( i e. { j e. S | ph } -> ( A. k e. { j e. S | ph } i <_ k -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) ) ) )
78 77 rexlimdv 
 |-  ( S C_ ( ZZ>= ` M ) -> ( E. i e. { j e. S | ph } A. k e. { j e. S | ph } i <_ k -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) ) )
79 78 adantr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> ( E. i e. { j e. S | ph } A. k e. { j e. S | ph } i <_ k -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) ) )
80 13 79 mpd 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )