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 𝐹 = recs ( 𝐺 )
Assertion tfr1a ( Fun 𝐹 ∧ Lim dom 𝐹 )

Proof

Step Hyp Ref Expression
1 tfr.1 𝐹 = recs ( 𝐺 )
2 eqid { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓𝑦 ) ) ) }
3 2 tfrlem7 Fun recs ( 𝐺 )
4 1 funeqi ( Fun 𝐹 ↔ Fun recs ( 𝐺 ) )
5 3 4 mpbir Fun 𝐹
6 2 tfrlem16 Lim dom recs ( 𝐺 )
7 1 dmeqi dom 𝐹 = dom recs ( 𝐺 )
8 limeq ( dom 𝐹 = dom recs ( 𝐺 ) → ( Lim dom 𝐹 ↔ Lim dom recs ( 𝐺 ) ) )
9 7 8 ax-mp ( Lim dom 𝐹 ↔ Lim dom recs ( 𝐺 ) )
10 6 9 mpbir Lim dom 𝐹
11 5 10 pm3.2i ( Fun 𝐹 ∧ Lim dom 𝐹 )