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	$⊢ F = recs (G)$
	Assertion	tfr1a	$⊢ (Fun F \land Lim dom F)$

Step	Hyp	Ref	Expression
1		tfr.1	$⊢ F = recs (G)$
2		eqid	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\}$
3	2	tfrlem7	$⊢ Fun recs (G)$
4	1	funeqi	$⊢ Fun F \leftrightarrow Fun recs (G)$
5	3 4	mpbir	$⊢ Fun F$
6	2	tfrlem16	$⊢ Lim dom recs (G)$
7	1	dmeqi	$⊢ dom F = dom recs (G)$
8		limeq	$⊢ dom F = dom recs (G) \to (Lim dom F \leftrightarrow Lim dom recs (G))$
9	7 8	ax-mp	$⊢ Lim dom F \leftrightarrow Lim dom recs (G)$
10	6 9	mpbir	$⊢ Lim dom F$
11	5 10	pm3.2i	$⊢ (Fun F \land Lim dom F)$

Metamath Proof Explorer