bnj1098

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj1098.1	$⊢ D = ω ∖ \{\emptyset\}$
	Assertion	bnj1098	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j))$

Proof

Step	Hyp	Ref	Expression
1		bnj1098.1	$⊢ D = ω ∖ \{\emptyset\}$
2		3anrev	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \leftrightarrow (n \in D \land i \in n \land i \neq \emptyset)$
3		df-3an	$⊢ (n \in D \land i \in n \land i \neq \emptyset) \leftrightarrow ((n \in D \land i \in n) \land i \neq \emptyset)$
4	2 3	bitri	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \leftrightarrow ((n \in D \land i \in n) \land i \neq \emptyset)$
5		simpr	$⊢ (n \in D \land i \in n) \to i \in n$
6	1	bnj923	$⊢ n \in D \to n \in ω$
7	6	adantr	$⊢ (n \in D \land i \in n) \to n \in ω$
8		elnn	$⊢ (i \in n \land n \in ω) \to i \in ω$
9	5 7 8	syl2anc	$⊢ (n \in D \land i \in n) \to i \in ω$
10	9	anim1i	$⊢ ((n \in D \land i \in n) \land i \neq \emptyset) \to (i \in ω \land i \neq \emptyset)$
11	4 10	sylbi	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \to (i \in ω \land i \neq \emptyset)$
12		nnsuc	$⊢ (i \in ω \land i \neq \emptyset) \to \exists j \in ω i = suc j$
13	11 12	syl	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \to \exists j \in ω i = suc j$
14		df-rex	$⊢ \exists j \in ω i = suc j \leftrightarrow \exists j (j \in ω \land i = suc j)$
15	14	imbi2i	$⊢ ((i \neq \emptyset \land i \in n \land n \in D) \to \exists j \in ω i = suc j) \leftrightarrow ((i \neq \emptyset \land i \in n \land n \in D) \to \exists j (j \in ω \land i = suc j))$
16		19.37v	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in ω \land i = suc j)) \leftrightarrow ((i \neq \emptyset \land i \in n \land n \in D) \to \exists j (j \in ω \land i = suc j))$
17	15 16	bitr4i	$⊢ ((i \neq \emptyset \land i \in n \land n \in D) \to \exists j \in ω i = suc j) \leftrightarrow \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in ω \land i = suc j))$
18	13 17	mpbi	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in ω \land i = suc j))$
19		ancr	$⊢ ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in ω \land i = suc j)) \to ((i \neq \emptyset \land i \in n \land n \in D) \to ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)))$
20	18 19	bnj101	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)))$
21		vex	$⊢ j \in V$
22	21	bnj216	$⊢ i = suc j \to j \in i$
23	22	ad2antlr	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to j \in i$
24		simpr2	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to i \in n$
25		3simpc	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \to (i \in n \land n \in D)$
26	25	ancomd	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \to (n \in D \land i \in n)$
27	26	adantl	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to (n \in D \land i \in n)$
28		nnord	$⊢ n \in ω \to Ord n$
29		ordtr1	$⊢ Ord n \to ((j \in i \land i \in n) \to j \in n)$
30	27 7 28 29	4syl	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to ((j \in i \land i \in n) \to j \in n)$
31	23 24 30	mp2and	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to j \in n$
32		simplr	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to i = suc j$
33	31 32	jca	$⊢ ((j \in ω \land i = suc j) \land (i \neq \emptyset \land i \in n \land n \in D)) \to (j \in n \land i = suc j)$
34	20 33	bnj1023	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j))$

Metamath Proof Explorer

Theorem bnj1098

Proof