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 \to (ψ \leftrightarrow χ)$
	infdesc.z	$⊢ y = z \to (ψ \leftrightarrow θ)$
	infdesc.s	$⊢ φ \to S \subseteq ℤ_{\geq M}$
	infdesc.1	$⊢ (φ \land (x \in S \land χ)) \to \exists z \in S (θ \land z < x)$
Assertion	infdesc	$⊢ φ \to \{y \in S \| ψ\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		infdesc.x	$⊢ y = x \to (ψ \leftrightarrow χ)$
2		infdesc.z	$⊢ y = z \to (ψ \leftrightarrow θ)$
3		infdesc.s	$⊢ φ \to S \subseteq ℤ_{\geq M}$
4		infdesc.1	$⊢ (φ \land (x \in S \land χ)) \to \exists z \in S (θ \land z < x)$
5		df-ne	$⊢ \{y \in S \| ψ\} \neq \emptyset \leftrightarrow \neg \{y \in S \| ψ\} = \emptyset$
6		ssrab2	$⊢ \{y \in S \| ψ\} \subseteq S$
7	6 3	sstrid	$⊢ φ \to \{y \in S \| ψ\} \subseteq ℤ_{\geq M}$
8		uzwo	$⊢ (\{y \in S \| ψ\} \subseteq ℤ_{\geq M} \land \{y \in S \| ψ\} \neq \emptyset) \to \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
9	7 8	sylan	$⊢ (φ \land \{y \in S \| ψ\} \neq \emptyset) \to \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
10	1	elrab	$⊢ x \in \{y \in S \| ψ\} \leftrightarrow (x \in S \land χ)$
11		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
12	3 11	sstrdi	$⊢ φ \to S \subseteq ℝ$
13	12	adantr	$⊢ (φ \land x \in S) \to S \subseteq ℝ$
14	13	sselda	$⊢ ((φ \land x \in S) \land z \in S) \to z \in ℝ$
15	12	sselda	$⊢ (φ \land x \in S) \to x \in ℝ$
16	15	adantr	$⊢ ((φ \land x \in S) \land z \in S) \to x \in ℝ$
17	14 16	ltnled	$⊢ ((φ \land x \in S) \land z \in S) \to (z < x \leftrightarrow \neg x \leq z)$
18	17	anbi2d	$⊢ ((φ \land x \in S) \land z \in S) \to ((θ \land z < x) \leftrightarrow (θ \land \neg x \leq z))$
19	18	rexbidva	$⊢ (φ \land x \in S) \to (\exists z \in S (θ \land z < x) \leftrightarrow \exists z \in S (θ \land \neg x \leq z))$
20	19	adantrr	$⊢ (φ \land (x \in S \land χ)) \to (\exists z \in S (θ \land z < x) \leftrightarrow \exists z \in S (θ \land \neg x \leq z))$
21	4 20	mpbid	$⊢ (φ \land (x \in S \land χ)) \to \exists z \in S (θ \land \neg x \leq z)$
22	10 21	sylan2b	$⊢ (φ \land x \in \{y \in S \| ψ\}) \to \exists z \in S (θ \land \neg x \leq z)$
23	2	rexrab	$⊢ \exists z \in \{y \in S \| ψ\} \neg x \leq z \leftrightarrow \exists z \in S (θ \land \neg x \leq z)$
24	22 23	sylibr	$⊢ (φ \land x \in \{y \in S \| ψ\}) \to \exists z \in \{y \in S \| ψ\} \neg x \leq z$
25	24	ralrimiva	$⊢ φ \to \forall x \in \{y \in S \| ψ\} \exists z \in \{y \in S \| ψ\} \neg x \leq z$
26		rexnal	$⊢ \exists z \in \{y \in S \| ψ\} \neg x \leq z \leftrightarrow \neg \forall z \in \{y \in S \| ψ\} x \leq z$
27	26	ralbii	$⊢ \forall x \in \{y \in S \| ψ\} \exists z \in \{y \in S \| ψ\} \neg x \leq z \leftrightarrow \forall x \in \{y \in S \| ψ\} \neg \forall z \in \{y \in S \| ψ\} x \leq z$
28		ralnex	$⊢ \forall x \in \{y \in S \| ψ\} \neg \forall z \in \{y \in S \| ψ\} x \leq z \leftrightarrow \neg \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
29	27 28	bitri	$⊢ \forall x \in \{y \in S \| ψ\} \exists z \in \{y \in S \| ψ\} \neg x \leq z \leftrightarrow \neg \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
30	25 29	sylib	$⊢ φ \to \neg \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
31	30	adantr	$⊢ (φ \land \{y \in S \| ψ\} \neq \emptyset) \to \neg \exists x \in \{y \in S \| ψ\} \forall z \in \{y \in S \| ψ\} x \leq z$
32	9 31	pm2.21dd	$⊢ (φ \land \{y \in S \| ψ\} \neq \emptyset) \to \{y \in S \| ψ\} = \emptyset$
33	5 32	sylan2br	$⊢ (φ \land \neg \{y \in S \| ψ\} = \emptyset) \to \{y \in S \| ψ\} = \emptyset$
34	33	pm2.18da	$⊢ φ \to \{y \in S \| ψ\} = \emptyset$

Metamath Proof Explorer

Theorem infdesc

Proof