bnj958

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	bnj958.1	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj958.2	$⊢ G = f \cup \{⟨n, C⟩\}$
Assertion	bnj958	$⊢ G (i) = f (i) \to \forall y G (i) = f (i)$

Proof

Step	Hyp	Ref	Expression
1		bnj958.1	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
2		bnj958.2	$⊢ G = f \cup \{⟨n, C⟩\}$
3		nfcv	$⊢ \underline{Ⅎ} y f$
4		nfcv	$⊢ \underline{Ⅎ} y n$
5		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in f (m)} pred (y, A, R)$
6	1 5	nfcxfr	$⊢ \underline{Ⅎ} y C$
7	4 6	nfop	$⊢ \underline{Ⅎ} y ⟨n, C⟩$
8	7	nfsn	$⊢ \underline{Ⅎ} y \{⟨n, C⟩\}$
9	3 8	nfun	$⊢ \underline{Ⅎ} y (f \cup \{⟨n, C⟩\})$
10	2 9	nfcxfr	$⊢ \underline{Ⅎ} y G$
11		nfcv	$⊢ \underline{Ⅎ} y i$
12	10 11	nffv	$⊢ \underline{Ⅎ} y G (i)$
13	12	nfeq1	$⊢ Ⅎ y G (i) = f (i)$
14	13	nf5ri	$⊢ G (i) = f (i) \to \forall y G (i) = f (i)$

Metamath Proof Explorer

Theorem bnj958

Proof