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

Metamath Proof Explorer

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 ) ) ) )