Theorem recsfnon

Description: Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Assertion	recsfnon	⊢ recs ( 𝐹 ) Fn On

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ recs ( 𝐹 ) = recs ( 𝐹 )
2	1	tfr1	⊢ recs ( 𝐹 ) Fn On