bnj986

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	bnj986.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj986.10	$⊢ D = ω ∖ \{\emptyset\}$
	bnj986.15	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
Assertion	bnj986	$⊢ χ \to \exists m \exists p τ$

Proof

Step	Hyp	Ref	Expression
1		bnj986.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
2		bnj986.10	$⊢ D = ω ∖ \{\emptyset\}$
3		bnj986.15	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
4	2	bnj158	$⊢ n \in D \to \exists m \in ω n = suc m$
5	1 4	bnj769	$⊢ χ \to \exists m \in ω n = suc m$
6	5	bnj1196	$⊢ χ \to \exists m (m \in ω \land n = suc m)$
7		vex	$⊢ n \in V$
8	7	sucex	$⊢ suc n \in V$
9	8	isseti	$⊢ \exists p p = suc n$
10	6 9	jctir	$⊢ χ \to (\exists m (m \in ω \land n = suc m) \land \exists p p = suc n)$
11		exdistr	$⊢ \exists m \exists p ((m \in ω \land n = suc m) \land p = suc n) \leftrightarrow \exists m ((m \in ω \land n = suc m) \land \exists p p = suc n)$
12		19.41v	$⊢ \exists m ((m \in ω \land n = suc m) \land \exists p p = suc n) \leftrightarrow (\exists m (m \in ω \land n = suc m) \land \exists p p = suc n)$
13	11 12	bitr2i	$⊢ (\exists m (m \in ω \land n = suc m) \land \exists p p = suc n) \leftrightarrow \exists m \exists p ((m \in ω \land n = suc m) \land p = suc n)$
14	10 13	sylib	$⊢ χ \to \exists m \exists p ((m \in ω \land n = suc m) \land p = suc n)$
15		df-3an	$⊢ (m \in ω \land n = suc m \land p = suc n) \leftrightarrow ((m \in ω \land n = suc m) \land p = suc n)$
16	3 15	bitri	$⊢ τ \leftrightarrow ((m \in ω \land n = suc m) \land p = suc n)$
17	16	2exbii	$⊢ \exists m \exists p τ \leftrightarrow \exists m \exists p ((m \in ω \land n = suc m) \land p = suc n)$
18	14 17	sylibr	$⊢ χ \to \exists m \exists p τ$

Metamath Proof Explorer

Theorem bnj986

Proof