peano5

Description: The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of TakeutiZaring p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as Theorem findes . (Contributed by NM, 18-Feb-2004) Avoid ax-10 , ax-12 . (Revised by GG, 3-Oct-2024)

		Ref	Expression
	Assertion	peano5	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to ω \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		eldifn	$⊢ z \in (ω ∖ A) \to \neg z \in A$
2	1	adantl	$⊢ ((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land z \in (ω ∖ A)) \to \neg z \in A$
3		eldifi	$⊢ z \in (ω ∖ A) \to z \in ω$
4		elndif	$⊢ \emptyset \in A \to \neg \emptyset \in (ω ∖ A)$
5		eleq1	$⊢ z = \emptyset \to (z \in (ω ∖ A) \leftrightarrow \emptyset \in (ω ∖ A))$
6	5	biimpcd	$⊢ z \in (ω ∖ A) \to (z = \emptyset \to \emptyset \in (ω ∖ A))$
7	6	necon3bd	$⊢ z \in (ω ∖ A) \to (\neg \emptyset \in (ω ∖ A) \to z \neq \emptyset)$
8	4 7	mpan9	$⊢ (\emptyset \in A \land z \in (ω ∖ A)) \to z \neq \emptyset$
9		nnsuc	$⊢ (z \in ω \land z \neq \emptyset) \to \exists y \in ω z = suc y$
10	3 8 9	syl2an2	$⊢ (\emptyset \in A \land z \in (ω ∖ A)) \to \exists y \in ω z = suc y$
11	10	ad4ant13	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land z \in (ω ∖ A)) \land (ω ∖ A) \cap z = \emptyset) \to \exists y \in ω z = suc y$
12		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
13		suceq	$⊢ x = y \to suc x = suc y$
14	13	eleq1d	$⊢ x = y \to (suc x \in A \leftrightarrow suc y \in A)$
15	12 14	imbi12d	$⊢ x = y \to ((x \in A \to suc x \in A) \leftrightarrow (y \in A \to suc y \in A))$
16	15	rspccv	$⊢ \forall x \in ω (x \in A \to suc x \in A) \to (y \in ω \to (y \in A \to suc y \in A))$
17		vex	$⊢ y \in V$
18	17	sucid	$⊢ y \in suc y$
19		eleq2	$⊢ z = suc y \to (y \in z \leftrightarrow y \in suc y)$
20	18 19	mpbiri	$⊢ z = suc y \to y \in z$
21		eleq1	$⊢ z = suc y \to (z \in ω \leftrightarrow suc y \in ω)$
22		peano2b	$⊢ y \in ω \leftrightarrow suc y \in ω$
23	21 22	bitr4di	$⊢ z = suc y \to (z \in ω \leftrightarrow y \in ω)$
24		minel	$⊢ (y \in z \land (ω ∖ A) \cap z = \emptyset) \to \neg y \in (ω ∖ A)$
25		neldif	$⊢ (y \in ω \land \neg y \in (ω ∖ A)) \to y \in A$
26	24 25	sylan2	$⊢ (y \in ω \land (y \in z \land (ω ∖ A) \cap z = \emptyset)) \to y \in A$
27	26	exp32	$⊢ y \in ω \to (y \in z \to ((ω ∖ A) \cap z = \emptyset \to y \in A))$
28	23 27	biimtrdi	$⊢ z = suc y \to (z \in ω \to (y \in z \to ((ω ∖ A) \cap z = \emptyset \to y \in A)))$
29	20 28	mpid	$⊢ z = suc y \to (z \in ω \to ((ω ∖ A) \cap z = \emptyset \to y \in A))$
30	3 29	syl5	$⊢ z = suc y \to (z \in (ω ∖ A) \to ((ω ∖ A) \cap z = \emptyset \to y \in A))$
31	30	impd	$⊢ z = suc y \to ((z \in (ω ∖ A) \land (ω ∖ A) \cap z = \emptyset) \to y \in A)$
32		eleq1a	$⊢ suc y \in A \to (z = suc y \to z \in A)$
33	32	com12	$⊢ z = suc y \to (suc y \in A \to z \in A)$
34	31 33	imim12d	$⊢ z = suc y \to ((y \in A \to suc y \in A) \to ((z \in (ω ∖ A) \land (ω ∖ A) \cap z = \emptyset) \to z \in A))$
35	34	com13	$⊢ (z \in (ω ∖ A) \land (ω ∖ A) \cap z = \emptyset) \to ((y \in A \to suc y \in A) \to (z = suc y \to z \in A))$
36	16 35	sylan9	$⊢ (\forall x \in ω (x \in A \to suc x \in A) \land (z \in (ω ∖ A) \land (ω ∖ A) \cap z = \emptyset)) \to (y \in ω \to (z = suc y \to z \in A))$
37	36	rexlimdv	$⊢ (\forall x \in ω (x \in A \to suc x \in A) \land (z \in (ω ∖ A) \land (ω ∖ A) \cap z = \emptyset)) \to (\exists y \in ω z = suc y \to z \in A)$
38	37	exp32	$⊢ \forall x \in ω (x \in A \to suc x \in A) \to (z \in (ω ∖ A) \to ((ω ∖ A) \cap z = \emptyset \to (\exists y \in ω z = suc y \to z \in A)))$
39	38	a1i	$⊢ \emptyset \in A \to (\forall x \in ω (x \in A \to suc x \in A) \to (z \in (ω ∖ A) \to ((ω ∖ A) \cap z = \emptyset \to (\exists y \in ω z = suc y \to z \in A))))$
40	39	imp41	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land z \in (ω ∖ A)) \land (ω ∖ A) \cap z = \emptyset) \to (\exists y \in ω z = suc y \to z \in A)$
41	11 40	mpd	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land z \in (ω ∖ A)) \land (ω ∖ A) \cap z = \emptyset) \to z \in A$
42	2 41	mtand	$⊢ ((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land z \in (ω ∖ A)) \to \neg (ω ∖ A) \cap z = \emptyset$
43	42	nrexdv	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to \neg \exists z \in (ω ∖ A) (ω ∖ A) \cap z = \emptyset$
44		ordom	$⊢ Ord ω$
45		difss	$⊢ ω ∖ A \subseteq ω$
46		tz7.5	$⊢ (Ord ω \land ω ∖ A \subseteq ω \land ω ∖ A \neq \emptyset) \to \exists z \in (ω ∖ A) (ω ∖ A) \cap z = \emptyset$
47	44 45 46	mp3an12	$⊢ ω ∖ A \neq \emptyset \to \exists z \in (ω ∖ A) (ω ∖ A) \cap z = \emptyset$
48	47	necon1bi	$⊢ \neg \exists z \in (ω ∖ A) (ω ∖ A) \cap z = \emptyset \to ω ∖ A = \emptyset$
49	43 48	syl	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to ω ∖ A = \emptyset$
50		ssdif0	$⊢ ω \subseteq A \leftrightarrow ω ∖ A = \emptyset$
51	49 50	sylibr	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to ω \subseteq A$

Metamath Proof Explorer

Theorem peano5

Proof