This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → { 𝑦 ∈ 𝑆 ∣ 𝜓 } = ∅ )