Metamath Proof Explorer


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 )