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 | x On f Fn x y x f y = F f y
tfrlem3.2 G V
Assertion tfrlem3a G A z On G Fn z w z G w = F G w

Proof

Step Hyp Ref Expression
1 tfrlem3.1 A = f | x On f Fn x y x f y = F f y
2 tfrlem3.2 G 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 y x f y = F f y w z G w = F G w
12 3 11 anbi12d f = G x = z f Fn x y x f y = F f y G Fn z w z G w = F G w
13 12 cbvrexdva f = G x On f Fn x y x f y = F f y z On G Fn z w z G w = F G w
14 2 13 1 elab2 G A z On G Fn z w z G w = F G w