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