Theorem tfrlem3a

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
Hypotheses	tfrlem3.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
	tfrlem3.2	|- G e. _V
Assertion	tfrlem3a	|- ( G e. A <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tfrlem3.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2		tfrlem3.2	|- G e. _V
3		fneq12	|- ( ( f = G /\ x = z ) -> ( f Fn x <-> G Fn z ) )
4		simpll	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> f = G )
5		simpr	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> y = w )
6	4 5	fveq12d	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> ( f ` y ) = ( G ` w ) )
7	4 5	reseq12d	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> ( f |` y ) = ( G |` w ) )
8	7	fveq2d	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> ( F ` ( f |` y ) ) = ( F ` ( G |` w ) ) )
9	6 8	eqeq12d	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> ( ( f ` y ) = ( F ` ( f |` y ) ) <-> ( G ` w ) = ( F ` ( G |` w ) ) ) )
10		simplr	|- ( ( ( f = G /\ x = z ) /\ y = w ) -> x = z )
11	9 10	cbvraldva2	|- ( ( f = G /\ x = z ) -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) <-> A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) )
12	3 11	anbi12d	|- ( ( f = G /\ x = z ) -> ( ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) <-> ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) ) )
13	12	cbvrexdva	|- ( f = G -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) ) )
14	2 13 1	elab2	|- ( G e. A <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) )