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 𝐹 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )