bnj1112

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
	Hypothesis	bnj1112.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	Assertion	bnj1112	$⊢ ψ \leftrightarrow \forall j ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$

Proof

Step	Hyp	Ref	Expression
1		bnj1112.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2	1	bnj115	$⊢ ψ \leftrightarrow \forall i ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		eleq1w	$⊢ i = j \to (i \in ω \leftrightarrow j \in ω)$
4		suceq	$⊢ i = j \to suc i = suc j$
5	4	eleq1d	$⊢ i = j \to (suc i \in n \leftrightarrow suc j \in n)$
6	3 5	anbi12d	$⊢ i = j \to ((i \in ω \land suc i \in n) \leftrightarrow (j \in ω \land suc j \in n))$
7	4	fveq2d	$⊢ i = j \to f (suc i) = f (suc j)$
8		fveq2	$⊢ i = j \to f (i) = f (j)$
9	8	bnj1113	$⊢ i = j \to ⋃_{y \in f (i)} pred (y, A, R) = ⋃_{y \in f (j)} pred (y, A, R)$
10	7 9	eqeq12d	$⊢ i = j \to (f (suc i) = ⋃_{y \in f (i)} pred (y, A, R) \leftrightarrow f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
11	6 10	imbi12d	$⊢ i = j \to (((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
12	11	cbvalvw	$⊢ \forall i ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall j ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
13	2 12	bitri	$⊢ ψ \leftrightarrow \forall j ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$

Metamath Proof Explorer

Theorem bnj1112

Proof