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 ⊢ 𝐹 = 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 𝐹 )