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 | x On f Fn x y x f y = F f y
Assertion tfrlem4 g A Fun g

Proof

Step Hyp Ref Expression
1 tfrlem.1 A = f | x On f Fn x y x f y = F f y
2 1 tfrlem3 A = g | z On g Fn z w z g w = F g w
3 2 abeq2i g A z On g Fn z w z g w = F g w
4 fnfun g Fn z Fun g
5 4 adantr g Fn z w z g w = F g w Fun g
6 5 rexlimivw z On g Fn z w z g w = F g w Fun g
7 3 6 sylbi g A Fun g