bnj1049

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	bnj1049.1	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
	bnj1049.2	$⊢ η \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
Assertion	bnj1049	$⊢ \forall i \in n η \leftrightarrow \forall i η$

Proof

Step	Hyp	Ref	Expression
1		bnj1049.1	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
2		bnj1049.2	$⊢ η \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
3		df-ral	$⊢ \forall i \in n η \leftrightarrow \forall i (i \in n \to η)$
4	2	imbi2i	$⊢ (i \in n \to η) \leftrightarrow (i \in n \to ((θ \land τ \land χ \land ζ) \to z \in B))$
5		impexp	$⊢ ((i \in n \land (θ \land τ \land χ \land ζ)) \to z \in B) \leftrightarrow (i \in n \to ((θ \land τ \land χ \land ζ) \to z \in B))$
6	4 5	bitr4i	$⊢ (i \in n \to η) \leftrightarrow ((i \in n \land (θ \land τ \land χ \land ζ)) \to z \in B)$
7	1	simplbi	$⊢ ζ \to i \in n$
8	7	bnj708	$⊢ (θ \land τ \land χ \land ζ) \to i \in n$
9	8	pm4.71ri	$⊢ (θ \land τ \land χ \land ζ) \leftrightarrow (i \in n \land (θ \land τ \land χ \land ζ))$
10	9	bicomi	$⊢ (i \in n \land (θ \land τ \land χ \land ζ)) \leftrightarrow (θ \land τ \land χ \land ζ)$
11	10	imbi1i	$⊢ ((i \in n \land (θ \land τ \land χ \land ζ)) \to z \in B) \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
12	6 11	bitri	$⊢ (i \in n \to η) \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
13	12 2	bitr4i	$⊢ (i \in n \to η) \leftrightarrow η$
14	13	albii	$⊢ \forall i (i \in n \to η) \leftrightarrow \forall i η$
15	3 14	bitri	$⊢ \forall i \in n η \leftrightarrow \forall i η$

Metamath Proof Explorer

Theorem bnj1049

Proof