This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \| E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f \|` y ) ) ) }
	Assertion	tfrlem4	\|- ( g e. A -> Fun g )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	\|- A = { f \| E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f \|` y ) ) ) }
2	1	tfrlem3	\|- A = { g \| E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g \|` w ) ) ) }
3	2	eqabri	\|- ( g e. A <-> E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g \|` w ) ) ) )
4		fnfun	\|- ( g Fn z -> Fun g )
5	4	adantr	\|- ( ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g \|` w ) ) ) -> Fun g )
6	5	rexlimivw	\|- ( E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g \|` w ) ) ) -> Fun g )
7	3 6	sylbi	\|- ( g e. A -> Fun g )