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