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|xOnfFnxyxfy=Ffy
Assertion tfrlem4 gAFung

Proof

Step Hyp Ref Expression
1 tfrlem.1 A=f|xOnfFnxyxfy=Ffy
2 1 tfrlem3 A=g|zOngFnzwzgw=Fgw
3 2 eqabri gAzOngFnzwzgw=Fgw
4 fnfun gFnzFung
5 4 adantr gFnzwzgw=FgwFung
6 5 rexlimivw zOngFnzwzgw=FgwFung
7 3 6 sylbi gAFung