bnj229

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

Proof

Step	Hyp	Ref	Expression
1		bnj229.1	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
2		bnj213	$⊢ pred (y, A, R) \subseteq A$
3	2	bnj226	$⊢ ⋃_{y \in F (m)} pred (y, A, R) \subseteq A$
4	1	bnj222	$⊢ ψ \leftrightarrow \forall m \in ω (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$
5	4	bnj228	$⊢ (m \in ω \land ψ) \to (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$
6	5	adantl	$⊢ (suc m = n \land (m \in ω \land ψ)) \to (suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R))$
7		eleq1	$⊢ suc m = n \to (suc m \in N \leftrightarrow n \in N)$
8		fveqeq2	$⊢ suc m = n \to (F (suc m) = ⋃_{y \in F (m)} pred (y, A, R) \leftrightarrow F (n) = ⋃_{y \in F (m)} pred (y, A, R))$
9	7 8	imbi12d	$⊢ suc m = n \to ((suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R)) \leftrightarrow (n \in N \to F (n) = ⋃_{y \in F (m)} pred (y, A, R)))$
10	9	adantr	$⊢ (suc m = n \land (m \in ω \land ψ)) \to ((suc m \in N \to F (suc m) = ⋃_{y \in F (m)} pred (y, A, R)) \leftrightarrow (n \in N \to F (n) = ⋃_{y \in F (m)} pred (y, A, R)))$
11	6 10	mpbid	$⊢ (suc m = n \land (m \in ω \land ψ)) \to (n \in N \to F (n) = ⋃_{y \in F (m)} pred (y, A, R))$
12	11	3impb	$⊢ (suc m = n \land m \in ω \land ψ) \to (n \in N \to F (n) = ⋃_{y \in F (m)} pred (y, A, R))$
13	12	impcom	$⊢ (n \in N \land (suc m = n \land m \in ω \land ψ)) \to F (n) = ⋃_{y \in F (m)} pred (y, A, R)$
14	3 13	bnj1262	$⊢ (n \in N \land (suc m = n \land m \in ω \land ψ)) \to F (n) \subseteq A$

Metamath Proof Explorer

Theorem bnj229

Proof