Metamath Proof Explorer

Theorem tfrlem3

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

		Ref	Expression
	Hypothesis	tfrlem3.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	Assertion	tfrlem3	$⊢ A = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))\}$

Proof

Step	Hyp	Ref	Expression
1		tfrlem3.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		vex	$⊢ g \in V$
3	1 2	tfrlem3a	$⊢ g \in A \leftrightarrow \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))$
4	3	eqabi	$⊢ A = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))\}$