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