bnj563

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

	Ref	Expression
Hypotheses	bnj563.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj563.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
Assertion	bnj563	$⊢ (η \land ρ) \to suc i \in m$

Proof

Step	Hyp	Ref	Expression
1		bnj563.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
2		bnj563.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
3		bnj312	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \leftrightarrow (n = suc m \land m \in D \land p \in ω \land m = suc p)$
4		bnj252	$⊢ (n = suc m \land m \in D \land p \in ω \land m = suc p) \leftrightarrow (n = suc m \land (m \in D \land p \in ω \land m = suc p))$
5	3 4	bitri	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \leftrightarrow (n = suc m \land (m \in D \land p \in ω \land m = suc p))$
6	5	simplbi	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \to n = suc m$
7	1 6	sylbi	$⊢ η \to n = suc m$
8	2	simp2bi	$⊢ ρ \to suc i \in n$
9	2	simp3bi	$⊢ ρ \to m \neq suc i$
10	8 9	jca	$⊢ ρ \to (suc i \in n \land m \neq suc i)$
11		necom	$⊢ m \neq suc i \leftrightarrow suc i \neq m$
12		eleq2	$⊢ n = suc m \to (suc i \in n \leftrightarrow suc i \in suc m)$
13	12	biimpa	$⊢ (n = suc m \land suc i \in n) \to suc i \in suc m$
14		elsuci	$⊢ suc i \in suc m \to (suc i \in m \lor suc i = m)$
15		orcom	$⊢ (suc i = m \lor suc i \in m) \leftrightarrow (suc i \in m \lor suc i = m)$
16		neor	$⊢ (suc i = m \lor suc i \in m) \leftrightarrow (suc i \neq m \to suc i \in m)$
17	15 16	bitr3i	$⊢ (suc i \in m \lor suc i = m) \leftrightarrow (suc i \neq m \to suc i \in m)$
18	14 17	sylib	$⊢ suc i \in suc m \to (suc i \neq m \to suc i \in m)$
19	18	imp	$⊢ (suc i \in suc m \land suc i \neq m) \to suc i \in m$
20	13 19	stoic3	$⊢ (n = suc m \land suc i \in n \land suc i \neq m) \to suc i \in m$
21	11 20	syl3an3b	$⊢ (n = suc m \land suc i \in n \land m \neq suc i) \to suc i \in m$
22	21	3expb	$⊢ (n = suc m \land (suc i \in n \land m \neq suc i)) \to suc i \in m$
23	7 10 22	syl2an	$⊢ (η \land ρ) \to suc i \in m$

Metamath Proof Explorer

Theorem bnj563

Proof