bnj222

Description: Technical lemma for bnj229 . 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
	Hypothesis	bnj222.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
	Assertion	bnj222	$⊢ ψ \leftrightarrow \forall m \in ω (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$

Proof

Step	Hyp	Ref	Expression
1		bnj222.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
2		suceq	$⊢ i = m \to suc i = suc m$
3	2	eleq1d	$⊢ i = m \to (suc i \in N \leftrightarrow suc m \in N)$
4	2	fveq2d	$⊢ i = m \to F (suc i) = F (suc m)$
5		fveq2	$⊢ i = m \to F (i) = F (m)$
6	5	bnj1113	$⊢ i = m \to ⋃_{y \in F (i)} pred (y, A, R) = ⋃_{y \in F (m)} pred (y, A, R)$
7	4 6	eqeq12d	$⊢ i = m \to (F (suc i) = ⋃_{y \in F (i)} pred (y, A, R) \leftrightarrow F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$
8	3 7	imbi12d	$⊢ i = m \to ((suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)) \leftrightarrow (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R)))$
9	8	cbvralvw	$⊢ \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)) \leftrightarrow \forall m \in ω (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$
10	1 9	bitri	$⊢ ψ \leftrightarrow \forall m \in ω (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$

Metamath Proof Explorer

Theorem bnj222

Proof