bnj1001

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1001.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1001.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
	bnj1001.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
	bnj1001.13	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1001.27	No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode \|-
Assertion	bnj1001	Could not format assertion : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj1001.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
2		bnj1001.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
3		bnj1001.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
4		bnj1001.13	$⊢ D = ω ∖ \{\emptyset\}$
5		bnj1001.27	Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode \|-
6	3	simplbi	$⊢ η \to i \in n$
7	6	bnj708	$⊢ (θ \land χ \land τ \land η) \to i \in n$
8	1	bnj1232	$⊢ χ \to n \in D$
9	8	bnj706	$⊢ (θ \land χ \land τ \land η) \to n \in D$
10	4	bnj923	$⊢ n \in D \to n \in ω$
11	9 10	syl	$⊢ (θ \land χ \land τ \land η) \to n \in ω$
12		elnn	$⊢ (i \in n \land n \in ω) \to i \in ω$
13	7 11 12	syl2anc	$⊢ (θ \land χ \land τ \land η) \to i \in ω$
14	2	simp3bi	$⊢ τ \to p = suc n$
15	14	bnj707	$⊢ (θ \land χ \land τ \land η) \to p = suc n$
16		nnord	$⊢ n \in ω \to Ord n$
17		ordsucelsuc	$⊢ Ord n \to (i \in n \leftrightarrow suc i \in suc n)$
18	10 16 17	3syl	$⊢ n \in D \to (i \in n \leftrightarrow suc i \in suc n)$
19	18	biimpa	$⊢ (n \in D \land i \in n) \to suc i \in suc n$
20		eleq2	$⊢ p = suc n \to (suc i \in p \leftrightarrow suc i \in suc n)$
21	19 20	anim12i	$⊢ ((n \in D \land i \in n) \land p = suc n) \to (suc i \in suc n \land (suc i \in p \leftrightarrow suc i \in suc n))$
22	9 7 15 21	syl21anc	$⊢ (θ \land χ \land τ \land η) \to (suc i \in suc n \land (suc i \in p \leftrightarrow suc i \in suc n))$
23		bianir	$⊢ (suc i \in suc n \land (suc i \in p \leftrightarrow suc i \in suc n)) \to suc i \in p$
24	22 23	syl	$⊢ (θ \land χ \land τ \land η) \to suc i \in p$
25	5 13 24	3jca	Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-

Metamath Proof Explorer

Theorem bnj1001

Proof