bnj168

Description: First-order logic and set theory. Revised to remove dependence on ax-reg . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by NM, 21-Dec-2016) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj168.1	$⊢ D = ω ∖ \{\emptyset\}$
	Assertion	bnj168	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in D n = suc m$

Proof

Step	Hyp	Ref	Expression
1		bnj168.1	$⊢ D = ω ∖ \{\emptyset\}$
2	1	bnj158	$⊢ n \in D \to \exists m \in ω n = suc m$
3	2	anim2i	$⊢ (n \neq 1_{𝑜} \land n \in D) \to (n \neq 1_{𝑜} \land \exists m \in ω n = suc m)$
4		r19.42v	$⊢ \exists m \in ω (n \neq 1_{𝑜} \land n = suc m) \leftrightarrow (n \neq 1_{𝑜} \land \exists m \in ω n = suc m)$
5	3 4	sylibr	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in ω (n \neq 1_{𝑜} \land n = suc m)$
6		neeq1	$⊢ n = suc m \to (n \neq 1_{𝑜} \leftrightarrow suc m \neq 1_{𝑜})$
7	6	biimpac	$⊢ (n \neq 1_{𝑜} \land n = suc m) \to suc m \neq 1_{𝑜}$
8		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
9	8	eqeq2i	$⊢ suc m = 1_{𝑜} \leftrightarrow suc m = suc \emptyset$
10		nnon	$⊢ m \in ω \to m \in On$
11		0elon	$⊢ \emptyset \in On$
12		suc11	$⊢ (m \in On \land \emptyset \in On) \to (suc m = suc \emptyset \leftrightarrow m = \emptyset)$
13	10 11 12	sylancl	$⊢ m \in ω \to (suc m = suc \emptyset \leftrightarrow m = \emptyset)$
14	9 13	bitr2id	$⊢ m \in ω \to (m = \emptyset \leftrightarrow suc m = 1_{𝑜})$
15	14	necon3bid	$⊢ m \in ω \to (m \neq \emptyset \leftrightarrow suc m \neq 1_{𝑜})$
16	7 15	syl5ibr	$⊢ m \in ω \to ((n \neq 1_{𝑜} \land n = suc m) \to m \neq \emptyset)$
17	16	ancld	$⊢ m \in ω \to ((n \neq 1_{𝑜} \land n = suc m) \to ((n \neq 1_{𝑜} \land n = suc m) \land m \neq \emptyset))$
18	17	reximia	$⊢ \exists m \in ω (n \neq 1_{𝑜} \land n = suc m) \to \exists m \in ω ((n \neq 1_{𝑜} \land n = suc m) \land m \neq \emptyset)$
19	5 18	syl	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in ω ((n \neq 1_{𝑜} \land n = suc m) \land m \neq \emptyset)$
20		anass	$⊢ ((n \neq 1_{𝑜} \land n = suc m) \land m \neq \emptyset) \leftrightarrow (n \neq 1_{𝑜} \land (n = suc m \land m \neq \emptyset))$
21	20	rexbii	$⊢ \exists m \in ω ((n \neq 1_{𝑜} \land n = suc m) \land m \neq \emptyset) \leftrightarrow \exists m \in ω (n \neq 1_{𝑜} \land (n = suc m \land m \neq \emptyset))$
22	19 21	sylib	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in ω (n \neq 1_{𝑜} \land (n = suc m \land m \neq \emptyset))$
23		simpr	$⊢ (n \neq 1_{𝑜} \land (n = suc m \land m \neq \emptyset)) \to (n = suc m \land m \neq \emptyset)$
24	22 23	bnj31	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in ω (n = suc m \land m \neq \emptyset)$
25		df-rex	$⊢ \exists m \in ω (n = suc m \land m \neq \emptyset) \leftrightarrow \exists m (m \in ω \land (n = suc m \land m \neq \emptyset))$
26	24 25	sylib	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m (m \in ω \land (n = suc m \land m \neq \emptyset))$
27		simpr	$⊢ (n = suc m \land m \neq \emptyset) \to m \neq \emptyset$
28	27	anim2i	$⊢ (m \in ω \land (n = suc m \land m \neq \emptyset)) \to (m \in ω \land m \neq \emptyset)$
29	1	eleq2i	$⊢ m \in D \leftrightarrow m \in (ω ∖ \{\emptyset\})$
30		eldifsn	$⊢ m \in (ω ∖ \{\emptyset\}) \leftrightarrow (m \in ω \land m \neq \emptyset)$
31	29 30	bitr2i	$⊢ (m \in ω \land m \neq \emptyset) \leftrightarrow m \in D$
32	28 31	sylib	$⊢ (m \in ω \land (n = suc m \land m \neq \emptyset)) \to m \in D$
33		simprl	$⊢ (m \in ω \land (n = suc m \land m \neq \emptyset)) \to n = suc m$
34	32 33	jca	$⊢ (m \in ω \land (n = suc m \land m \neq \emptyset)) \to (m \in D \land n = suc m)$
35	34	eximi	$⊢ \exists m (m \in ω \land (n = suc m \land m \neq \emptyset)) \to \exists m (m \in D \land n = suc m)$
36	26 35	syl	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m (m \in D \land n = suc m)$
37		df-rex	$⊢ \exists m \in D n = suc m \leftrightarrow \exists m (m \in D \land n = suc m)$
38	36 37	sylibr	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in D n = suc m$

Metamath Proof Explorer

Theorem bnj168

Proof