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 ψ χ
infdesc.z y = z ψ θ
infdesc.s φ S M
infdesc.1 φ x S χ z S θ z < x
Assertion infdesc φ y S | ψ =

Proof

Step Hyp Ref Expression
1 infdesc.x y = x ψ χ
2 infdesc.z y = z ψ θ
3 infdesc.s φ S M
4 infdesc.1 φ x S χ z S θ z < x
5 df-ne y S | ψ ¬ y S | ψ =
6 ssrab2 y S | ψ S
7 6 3 sstrid φ y S | ψ M
8 uzwo y S | ψ M y S | ψ x y S | ψ z y S | ψ x z
9 7 8 sylan φ y S | ψ x y S | ψ z y S | ψ x z
10 1 elrab x y S | ψ x S χ
11 uzssre M
12 3 11 sstrdi φ S
13 12 adantr φ x S S
14 13 sselda φ x S z S z
15 12 sselda φ x S x
16 15 adantr φ x S z S x
17 14 16 ltnled φ x S z S z < x ¬ x z
18 17 anbi2d φ x S z S θ z < x θ ¬ x z
19 18 rexbidva φ x S z S θ z < x z S θ ¬ x z
20 19 adantrr φ x S χ z S θ z < x z S θ ¬ x z
21 4 20 mpbid φ x S χ z S θ ¬ x z
22 10 21 sylan2b φ x y S | ψ z S θ ¬ x z
23 2 rexrab z y S | ψ ¬ x z z S θ ¬ x z
24 22 23 sylibr φ x y S | ψ z y S | ψ ¬ x z
25 24 ralrimiva φ x y S | ψ z y S | ψ ¬ x z
26 rexnal z y S | ψ ¬ x z ¬ z y S | ψ x z
27 26 ralbii x y S | ψ z y S | ψ ¬ x z x y S | ψ ¬ z y S | ψ x z
28 ralnex x y S | ψ ¬ z y S | ψ x z ¬ x y S | ψ z y S | ψ x z
29 27 28 bitri x y S | ψ z y S | ψ ¬ x z ¬ x y S | ψ z y S | ψ x z
30 25 29 sylib φ ¬ x y S | ψ z y S | ψ x z
31 30 adantr φ y S | ψ ¬ x y S | ψ z y S | ψ x z
32 9 31 pm2.21dd φ y S | ψ y S | ψ =
33 5 32 sylan2br φ ¬ y S | ψ = y S | ψ =
34 33 pm2.18da φ y S | ψ =