npomex

Description: A simplifying observation, and an indication of why any attempt to develop a theory of the real numbers without the Axiom of Infinity is doomed to failure: since every member of P. is an infinite set, the negation of Infinity implies that P. , and hence RR , is empty. (Note that this proof, which used the fact that Dedekind cuts have no maximum, could just as well have used that they have no minimum, since they are downward-closed by prcdnq and nsmallnq ). (Contributed by Mario Carneiro, 11-May-2013) (Revised by Mario Carneiro, 16-Nov-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	npomex	$⊢ A \in 𝑷 \to ω \in V$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in 𝑷 \to A \in V$
2		prnmax	$⊢ (A \in 𝑷 \land x \in A) \to \exists y \in A x <_{𝑸} y$
3	2	ralrimiva	$⊢ A \in 𝑷 \to \forall x \in A \exists y \in A x <_{𝑸} y$
4		prpssnq	$⊢ A \in 𝑷 \to A \subset 𝑸$
5	4	pssssd	$⊢ A \in 𝑷 \to A \subseteq 𝑸$
6		ltsonq	$⊢ <_{𝑸} Or 𝑸$
7		soss	$⊢ A \subseteq 𝑸 \to (<_{𝑸} Or 𝑸 \to <_{𝑸} Or A)$
8	5 6 7	mpisyl	$⊢ A \in 𝑷 \to <_{𝑸} Or A$
9	8	adantr	$⊢ (A \in 𝑷 \land A \in Fin) \to <_{𝑸} Or A$
10		simpr	$⊢ (A \in 𝑷 \land A \in Fin) \to A \in Fin$
11		prn0	$⊢ A \in 𝑷 \to A \neq \emptyset$
12	11	adantr	$⊢ (A \in 𝑷 \land A \in Fin) \to A \neq \emptyset$
13		fimax2g	$⊢ (<_{𝑸} Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x <_{𝑸} y$
14	9 10 12 13	syl3anc	$⊢ (A \in 𝑷 \land A \in Fin) \to \exists x \in A \forall y \in A \neg x <_{𝑸} y$
15		ralnex	$⊢ \forall y \in A \neg x <_{𝑸} y \leftrightarrow \neg \exists y \in A x <_{𝑸} y$
16	15	rexbii	$⊢ \exists x \in A \forall y \in A \neg x <_{𝑸} y \leftrightarrow \exists x \in A \neg \exists y \in A x <_{𝑸} y$
17		rexnal	$⊢ \exists x \in A \neg \exists y \in A x <_{𝑸} y \leftrightarrow \neg \forall x \in A \exists y \in A x <_{𝑸} y$
18	16 17	bitri	$⊢ \exists x \in A \forall y \in A \neg x <_{𝑸} y \leftrightarrow \neg \forall x \in A \exists y \in A x <_{𝑸} y$
19	14 18	sylib	$⊢ (A \in 𝑷 \land A \in Fin) \to \neg \forall x \in A \exists y \in A x <_{𝑸} y$
20	19	ex	$⊢ A \in 𝑷 \to (A \in Fin \to \neg \forall x \in A \exists y \in A x <_{𝑸} y)$
21	3 20	mt2d	$⊢ A \in 𝑷 \to \neg A \in Fin$
22		nelne1	$⊢ (A \in V \land \neg A \in Fin) \to V \neq Fin$
23	1 21 22	syl2anc	$⊢ A \in 𝑷 \to V \neq Fin$
24	23	necomd	$⊢ A \in 𝑷 \to Fin \neq V$
25		fineqv	$⊢ \neg ω \in V \leftrightarrow Fin = V$
26	25	necon1abii	$⊢ Fin \neq V \leftrightarrow ω \in V$
27	24 26	sylib	$⊢ A \in 𝑷 \to ω \in V$

Metamath Proof Explorer

Theorem npomex

Proof