Metamath Proof Explorer

Theorem tfrlem4

Description: Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995)

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

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2	1	tfrlem3	$⊢ A = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))\}$
3	2	abeq2i	$⊢ g \in A \leftrightarrow \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))$
4		fnfun	$⊢ g Fn z \to Fun g$
5	4	adantr	$⊢ (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to Fun g$
6	5	rexlimivw	$⊢ \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to Fun g$
7	3 6	sylbi	$⊢ g \in A \to Fun g$