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 ( 𝑦 = 𝑥 → ( 𝜓𝜒 ) )
infdesc.z ( 𝑦 = 𝑧 → ( 𝜓𝜃 ) )
infdesc.s ( 𝜑𝑆 ⊆ ( ℤ𝑀 ) )
infdesc.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝜒 ) ) → ∃ 𝑧𝑆 ( 𝜃𝑧 < 𝑥 ) )
Assertion infdesc ( 𝜑 → { 𝑦𝑆𝜓 } = ∅ )

Proof

Step Hyp Ref Expression
1 infdesc.x ( 𝑦 = 𝑥 → ( 𝜓𝜒 ) )
2 infdesc.z ( 𝑦 = 𝑧 → ( 𝜓𝜃 ) )
3 infdesc.s ( 𝜑𝑆 ⊆ ( ℤ𝑀 ) )
4 infdesc.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝜒 ) ) → ∃ 𝑧𝑆 ( 𝜃𝑧 < 𝑥 ) )
5 df-ne ( { 𝑦𝑆𝜓 } ≠ ∅ ↔ ¬ { 𝑦𝑆𝜓 } = ∅ )
6 ssrab2 { 𝑦𝑆𝜓 } ⊆ 𝑆
7 6 3 sstrid ( 𝜑 → { 𝑦𝑆𝜓 } ⊆ ( ℤ𝑀 ) )
8 uzwo ( ( { 𝑦𝑆𝜓 } ⊆ ( ℤ𝑀 ) ∧ { 𝑦𝑆𝜓 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
9 7 8 sylan ( ( 𝜑 ∧ { 𝑦𝑆𝜓 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
10 1 elrab ( 𝑥 ∈ { 𝑦𝑆𝜓 } ↔ ( 𝑥𝑆𝜒 ) )
11 uzssre ( ℤ𝑀 ) ⊆ ℝ
12 3 11 sstrdi ( 𝜑𝑆 ⊆ ℝ )
13 12 adantr ( ( 𝜑𝑥𝑆 ) → 𝑆 ⊆ ℝ )
14 13 sselda ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑧𝑆 ) → 𝑧 ∈ ℝ )
15 12 sselda ( ( 𝜑𝑥𝑆 ) → 𝑥 ∈ ℝ )
16 15 adantr ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑧𝑆 ) → 𝑥 ∈ ℝ )
17 14 16 ltnled ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑧𝑆 ) → ( 𝑧 < 𝑥 ↔ ¬ 𝑥𝑧 ) )
18 17 anbi2d ( ( ( 𝜑𝑥𝑆 ) ∧ 𝑧𝑆 ) → ( ( 𝜃𝑧 < 𝑥 ) ↔ ( 𝜃 ∧ ¬ 𝑥𝑧 ) ) )
19 18 rexbidva ( ( 𝜑𝑥𝑆 ) → ( ∃ 𝑧𝑆 ( 𝜃𝑧 < 𝑥 ) ↔ ∃ 𝑧𝑆 ( 𝜃 ∧ ¬ 𝑥𝑧 ) ) )
20 19 adantrr ( ( 𝜑 ∧ ( 𝑥𝑆𝜒 ) ) → ( ∃ 𝑧𝑆 ( 𝜃𝑧 < 𝑥 ) ↔ ∃ 𝑧𝑆 ( 𝜃 ∧ ¬ 𝑥𝑧 ) ) )
21 4 20 mpbid ( ( 𝜑 ∧ ( 𝑥𝑆𝜒 ) ) → ∃ 𝑧𝑆 ( 𝜃 ∧ ¬ 𝑥𝑧 ) )
22 10 21 sylan2b ( ( 𝜑𝑥 ∈ { 𝑦𝑆𝜓 } ) → ∃ 𝑧𝑆 ( 𝜃 ∧ ¬ 𝑥𝑧 ) )
23 2 rexrab ( ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 ↔ ∃ 𝑧𝑆 ( 𝜃 ∧ ¬ 𝑥𝑧 ) )
24 22 23 sylibr ( ( 𝜑𝑥 ∈ { 𝑦𝑆𝜓 } ) → ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 )
25 24 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ { 𝑦𝑆𝜓 } ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 )
26 rexnal ( ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 ↔ ¬ ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
27 26 ralbii ( ∀ 𝑥 ∈ { 𝑦𝑆𝜓 } ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 ↔ ∀ 𝑥 ∈ { 𝑦𝑆𝜓 } ¬ ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
28 ralnex ( ∀ 𝑥 ∈ { 𝑦𝑆𝜓 } ¬ ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 ↔ ¬ ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
29 27 28 bitri ( ∀ 𝑥 ∈ { 𝑦𝑆𝜓 } ∃ 𝑧 ∈ { 𝑦𝑆𝜓 } ¬ 𝑥𝑧 ↔ ¬ ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
30 25 29 sylib ( 𝜑 → ¬ ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
31 30 adantr ( ( 𝜑 ∧ { 𝑦𝑆𝜓 } ≠ ∅ ) → ¬ ∃ 𝑥 ∈ { 𝑦𝑆𝜓 } ∀ 𝑧 ∈ { 𝑦𝑆𝜓 } 𝑥𝑧 )
32 9 31 pm2.21dd ( ( 𝜑 ∧ { 𝑦𝑆𝜓 } ≠ ∅ ) → { 𝑦𝑆𝜓 } = ∅ )
33 5 32 sylan2br ( ( 𝜑 ∧ ¬ { 𝑦𝑆𝜓 } = ∅ ) → { 𝑦𝑆𝜓 } = ∅ )
34 33 pm2.18da ( 𝜑 → { 𝑦𝑆𝜓 } = ∅ )