Metamath Proof Explorer

Theorem infdesc

Description: Infinite descent. The hypotheses say that S is lower bounded, and that if ps holds for an integer in S , it holds for a smaller integer in S . By infinite descent, eventually we cannot go any smaller, therefore ps holds for no integer in S . (Contributed by SN, 20-Aug-2024)

Ref Expression
Hypotheses infdesc.x 
|- ( y = x -> ( ps <-> ch ) )
infdesc.z 
|- ( y = z -> ( ps <-> th ) )
infdesc.s 
|- ( ph -> S C_ ( ZZ>= ` M ) )
infdesc.1 
|- ( ( ph /\ ( x e. S /\ ch ) ) -> E. z e. S ( th /\ z < x ) )
Assertion infdesc 
|- ( ph -> { y e. S | ps } = (/) )

Proof

Step Hyp Ref Expression
1 infdesc.x 
 |-  ( y = x -> ( ps <-> ch ) )
2 infdesc.z 
 |-  ( y = z -> ( ps <-> th ) )
3 infdesc.s 
 |-  ( ph -> S C_ ( ZZ>= ` M ) )
4 infdesc.1 
 |-  ( ( ph /\ ( x e. S /\ ch ) ) -> E. z e. S ( th /\ z < x ) )
5 df-ne 
 |-  ( { y e. S | ps } =/= (/) <-> -. { y e. S | ps } = (/) )
6 ssrab2 
 |-  { y e. S | ps } C_ S
7 6 3 sstrid 
 |-  ( ph -> { y e. S | ps } C_ ( ZZ>= ` M ) )
8 uzwo 
 |-  ( ( { y e. S | ps } C_ ( ZZ>= ` M ) /\ { y e. S | ps } =/= (/) ) -> E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
9 7 8 sylan 
 |-  ( ( ph /\ { y e. S | ps } =/= (/) ) -> E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
10 1 elrab 
 |-  ( x e. { y e. S | ps } <-> ( x e. S /\ ch ) )
11 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
12 3 11 sstrdi 
 |-  ( ph -> S C_ RR )
13 12 adantr 
 |-  ( ( ph /\ x e. S ) -> S C_ RR )
14 13 sselda 
 |-  ( ( ( ph /\ x e. S ) /\ z e. S ) -> z e. RR )
15 12 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. RR )
16 15 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ z e. S ) -> x e. RR )
17 14 16 ltnled 
 |-  ( ( ( ph /\ x e. S ) /\ z e. S ) -> ( z < x <-> -. x <_ z ) )
18 17 anbi2d 
 |-  ( ( ( ph /\ x e. S ) /\ z e. S ) -> ( ( th /\ z < x ) <-> ( th /\ -. x <_ z ) ) )
19 18 rexbidva 
 |-  ( ( ph /\ x e. S ) -> ( E. z e. S ( th /\ z < x ) <-> E. z e. S ( th /\ -. x <_ z ) ) )
20 19 adantrr 
 |-  ( ( ph /\ ( x e. S /\ ch ) ) -> ( E. z e. S ( th /\ z < x ) <-> E. z e. S ( th /\ -. x <_ z ) ) )
21 4 20 mpbid 
 |-  ( ( ph /\ ( x e. S /\ ch ) ) -> E. z e. S ( th /\ -. x <_ z ) )
22 10 21 sylan2b 
 |-  ( ( ph /\ x e. { y e. S | ps } ) -> E. z e. S ( th /\ -. x <_ z ) )
23 2 rexrab 
 |-  ( E. z e. { y e. S | ps } -. x <_ z <-> E. z e. S ( th /\ -. x <_ z ) )
24 22 23 sylibr 
 |-  ( ( ph /\ x e. { y e. S | ps } ) -> E. z e. { y e. S | ps } -. x <_ z )
25 24 ralrimiva 
 |-  ( ph -> A. x e. { y e. S | ps } E. z e. { y e. S | ps } -. x <_ z )
26 rexnal 
 |-  ( E. z e. { y e. S | ps } -. x <_ z <-> -. A. z e. { y e. S | ps } x <_ z )
27 26 ralbii 
 |-  ( A. x e. { y e. S | ps } E. z e. { y e. S | ps } -. x <_ z <-> A. x e. { y e. S | ps } -. A. z e. { y e. S | ps } x <_ z )
28 ralnex 
 |-  ( A. x e. { y e. S | ps } -. A. z e. { y e. S | ps } x <_ z <-> -. E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
29 27 28 bitri 
 |-  ( A. x e. { y e. S | ps } E. z e. { y e. S | ps } -. x <_ z <-> -. E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
30 25 29 sylib 
 |-  ( ph -> -. E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
31 30 adantr 
 |-  ( ( ph /\ { y e. S | ps } =/= (/) ) -> -. E. x e. { y e. S | ps } A. z e. { y e. S | ps } x <_ z )
32 9 31 pm2.21dd 
 |-  ( ( ph /\ { y e. S | ps } =/= (/) ) -> { y e. S | ps } = (/) )
33 5 32 sylan2br 
 |-  ( ( ph /\ -. { y e. S | ps } = (/) ) -> { y e. S | ps } = (/) )
34 33 pm2.18da 
 |-  ( ph -> { y e. S | ps } = (/) )