This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )