bnj953

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

Proof

Step	Hyp	Ref	Expression
1		bnj953.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2		bnj953.2	$⊢ G (i) = f (i) \to \forall y G (i) = f (i)$
3		bnj312	$⊢ (G (i) = f (i) \land G (suc i) = f (suc i) \land (i \in ω \land suc i \in n) \land ψ) \leftrightarrow (G (suc i) = f (suc i) \land G (i) = f (i) \land (i \in ω \land suc i \in n) \land ψ)$
4		bnj251	$⊢ (G (suc i) = f (suc i) \land G (i) = f (i) \land (i \in ω \land suc i \in n) \land ψ) \leftrightarrow (G (suc i) = f (suc i) \land (G (i) = f (i) \land ((i \in ω \land suc i \in n) \land ψ)))$
5	3 4	bitri	$⊢ (G (i) = f (i) \land G (suc i) = f (suc i) \land (i \in ω \land suc i \in n) \land ψ) \leftrightarrow (G (suc i) = f (suc i) \land (G (i) = f (i) \land ((i \in ω \land suc i \in n) \land ψ)))$
6	1	bnj115	$⊢ ψ \leftrightarrow \forall i ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
7		sp	$⊢ \forall i ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \to ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
8	7	impcom	$⊢ ((i \in ω \land suc i \in n) \land \forall i ((i \in ω \land suc i \in n) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
9	6 8	sylan2b	$⊢ ((i \in ω \land suc i \in n) \land ψ) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
10	2	bnj956	$⊢ G (i) = f (i) \to ⋃_{y \in G (i)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
11		eqtr3	$⊢ (f (suc i) = ⋃_{y \in f (i)} pred (y, A, R) \land ⋃_{y \in G (i)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)) \to f (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
12	9 10 11	syl2anr	$⊢ (G (i) = f (i) \land ((i \in ω \land suc i \in n) \land ψ)) \to f (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
13		eqtr	$⊢ (G (suc i) = f (suc i) \land f (suc i) = ⋃_{y \in G (i)} pred (y, A, R)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
14	12 13	sylan2	$⊢ (G (suc i) = f (suc i) \land (G (i) = f (i) \land ((i \in ω \land suc i \in n) \land ψ))) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
15	5 14	sylbi	$⊢ (G (i) = f (i) \land G (suc i) = f (suc i) \land (i \in ω \land suc i \in n) \land ψ) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$

Metamath Proof Explorer

Theorem bnj953

Proof