Theorem tfr1a

Description: A weak version of tfr1 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Hypothesis	tfr.1	|- F = recs ( G )
Assertion	tfr1a	|- ( Fun F /\ Lim dom F )

Proof

Step	Hyp	Ref	Expression
1		tfr.1	|- F = recs ( G )
2		eqid	|- { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
3	2	tfrlem7	|- Fun recs ( G )
4	1	funeqi	|- ( Fun F <-> Fun recs ( G ) )
5	3 4	mpbir	|- Fun F
6	2	tfrlem16	|- Lim dom recs ( G )
7	1	dmeqi	|- dom F = dom recs ( G )
8		limeq	|- ( dom F = dom recs ( G ) -> ( Lim dom F <-> Lim dom recs ( G ) ) )
9	7 8	ax-mp	|- ( Lim dom F <-> Lim dom recs ( G ) )
10	6 9	mpbir	|- Lim dom F
11	5 10	pm3.2i	|- ( Fun F /\ Lim dom F )