peano5OLD

Description: Obsolete version of peano5 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	peano5OLD	$⊢ (\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	$⊢ y \in (ω ∖ A) \to \neg y \in A$
2	1	adantl	$⊢ ((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land y \in (ω ∖ A)) \to \neg y \in A$
3		eldifi	$⊢ y \in (ω ∖ A) \to y \in ω$
4		elndif	$⊢ \emptyset \in A \to \neg \emptyset \in (ω ∖ A)$
5		eleq1	$⊢ y = \emptyset \to (y \in (ω ∖ A) \leftrightarrow \emptyset \in (ω ∖ A))$
6	5	biimpcd	$⊢ y \in (ω ∖ A) \to (y = \emptyset \to \emptyset \in (ω ∖ A))$
7	6	necon3bd	$⊢ y \in (ω ∖ A) \to (\neg \emptyset \in (ω ∖ A) \to y \neq \emptyset)$
8	4 7	mpan9	$⊢ (\emptyset \in A \land y \in (ω ∖ A)) \to y \neq \emptyset$
9		nnsuc	$⊢ (y \in ω \land y \neq \emptyset) \to \exists x \in ω y = suc x$
10	3 8 9	syl2an2	$⊢ (\emptyset \in A \land y \in (ω ∖ A)) \to \exists x \in ω y = suc x$
11	10	ad4ant13	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land y \in (ω ∖ A)) \land (ω ∖ A) \cap y = \emptyset) \to \exists x \in ω y = suc x$
12		nfra1	$⊢ Ⅎ x \forall x \in ω (x \in A \to suc x \in A)$
13		nfv	$⊢ Ⅎ x (y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset)$
14	12 13	nfan	$⊢ Ⅎ x (\forall x \in ω (x \in A \to suc x \in A) \land (y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset))$
15		nfv	$⊢ Ⅎ x y \in A$
16		rsp	$⊢ \forall x \in ω (x \in A \to suc x \in A) \to (x \in ω \to (x \in A \to suc x \in A))$
17		vex	$⊢ x \in V$
18	17	sucid	$⊢ x \in suc x$
19		eleq2	$⊢ y = suc x \to (x \in y \leftrightarrow x \in suc x)$
20	18 19	mpbiri	$⊢ y = suc x \to x \in y$
21		eleq1	$⊢ y = suc x \to (y \in ω \leftrightarrow suc x \in ω)$
22		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
23	21 22	bitr4di	$⊢ y = suc x \to (y \in ω \leftrightarrow x \in ω)$
24		minel	$⊢ (x \in y \land (ω ∖ A) \cap y = \emptyset) \to \neg x \in (ω ∖ A)$
25		neldif	$⊢ (x \in ω \land \neg x \in (ω ∖ A)) \to x \in A$
26	24 25	sylan2	$⊢ (x \in ω \land (x \in y \land (ω ∖ A) \cap y = \emptyset)) \to x \in A$
27	26	exp32	$⊢ x \in ω \to (x \in y \to ((ω ∖ A) \cap y = \emptyset \to x \in A))$
28	23 27	syl6bi	$⊢ y = suc x \to (y \in ω \to (x \in y \to ((ω ∖ A) \cap y = \emptyset \to x \in A)))$
29	20 28	mpid	$⊢ y = suc x \to (y \in ω \to ((ω ∖ A) \cap y = \emptyset \to x \in A))$
30	3 29	syl5	$⊢ y = suc x \to (y \in (ω ∖ A) \to ((ω ∖ A) \cap y = \emptyset \to x \in A))$
31	30	impd	$⊢ y = suc x \to ((y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset) \to x \in A)$
32		eleq1a	$⊢ suc x \in A \to (y = suc x \to y \in A)$
33	32	com12	$⊢ y = suc x \to (suc x \in A \to y \in A)$
34	31 33	imim12d	$⊢ y = suc x \to ((x \in A \to suc x \in A) \to ((y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset) \to y \in A))$
35	34	com13	$⊢ (y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset) \to ((x \in A \to suc x \in A) \to (y = suc x \to y \in A))$
36	16 35	sylan9	$⊢ (\forall x \in ω (x \in A \to suc x \in A) \land (y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset)) \to (x \in ω \to (y = suc x \to y \in A))$
37	14 15 36	rexlimd	$⊢ (\forall x \in ω (x \in A \to suc x \in A) \land (y \in (ω ∖ A) \land (ω ∖ A) \cap y = \emptyset)) \to (\exists x \in ω y = suc x \to y \in A)$
38	37	exp32	$⊢ \forall x \in ω (x \in A \to suc x \in A) \to (y \in (ω ∖ A) \to ((ω ∖ A) \cap y = \emptyset \to (\exists x \in ω y = suc x \to y \in A)))$
39	38	a1i	$⊢ \emptyset \in A \to (\forall x \in ω (x \in A \to suc x \in A) \to (y \in (ω ∖ A) \to ((ω ∖ A) \cap y = \emptyset \to (\exists x \in ω y = suc x \to y \in A))))$
40	39	imp41	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land y \in (ω ∖ A)) \land (ω ∖ A) \cap y = \emptyset) \to (\exists x \in ω y = suc x \to y \in A)$
41	11 40	mpd	$⊢ (((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land y \in (ω ∖ A)) \land (ω ∖ A) \cap y = \emptyset) \to y \in A$
42	2 41	mtand	$⊢ ((\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \land y \in (ω ∖ A)) \to \neg (ω ∖ A) \cap y = \emptyset$
43	42	nrexdv	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to \neg \exists y \in (ω ∖ A) (ω ∖ A) \cap y = \emptyset$
44		ordom	$⊢ Ord ω$
45		difss	$⊢ ω ∖ A \subseteq ω$
46		tz7.5	$⊢ (Ord ω \land ω ∖ A \subseteq ω \land ω ∖ A \neq \emptyset) \to \exists y \in (ω ∖ A) (ω ∖ A) \cap y = \emptyset$
47	44 45 46	mp3an12	$⊢ ω ∖ A \neq \emptyset \to \exists y \in (ω ∖ A) (ω ∖ A) \cap y = \emptyset$
48	47	necon1bi	$⊢ \neg \exists y \in (ω ∖ A) (ω ∖ A) \cap y = \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 peano5OLD

Proof