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

Metamath Proof Explorer

Theorem tfr2a

Description: A weak version of tfr2 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 tfr2a ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tfr.1 ⊢ 𝐹 = recs ( 𝐺 )
2 eqid ⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
3 2 tfrlem9 ⊢ ( 𝐴 ∈ dom recs ( 𝐺 ) → ( recs ( 𝐺 ) ‘ 𝐴 ) = ( 𝐺 ‘ ( recs ( 𝐺 ) ↾ 𝐴 ) ) )
4 1 dmeqi ⊢ dom 𝐹 = dom recs ( 𝐺 )
5 3 4 eleq2s ⊢ ( 𝐴 ∈ dom 𝐹 → ( recs ( 𝐺 ) ‘ 𝐴 ) = ( 𝐺 ‘ ( recs ( 𝐺 ) ↾ 𝐴 ) ) )
6 1 fveq1i ⊢ ( 𝐹 ‘ 𝐴 ) = ( recs ( 𝐺 ) ‘ 𝐴 )
7 1 reseq1i ⊢ ( 𝐹 ↾ 𝐴 ) = ( recs ( 𝐺 ) ↾ 𝐴 )
8 7 fveq2i ⊢ ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) = ( 𝐺 ‘ ( recs ( 𝐺 ) ↾ 𝐴 ) )
9 5 6 8 3eqtr4g ⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )