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

Metamath Proof Explorer

Theorem tfrlem6

Description: Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

		Ref	Expression
	Hypothesis	tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	Assertion	tfrlem6	$⊢ Rel recs (F)$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		reluni	$⊢ Rel ⋃ A \leftrightarrow \forall g \in A Rel g$
3	1	tfrlem4	$⊢ g \in A \to Fun g$
4		funrel	$⊢ Fun g \to Rel g$
5	3 4	syl	$⊢ g \in A \to Rel g$
6	2 5	mprgbir	$⊢ Rel ⋃ A$
7	1	recsfval	$⊢ recs (F) = ⋃ A$
8	7	releqi	$⊢ Rel recs (F) \leftrightarrow Rel ⋃ A$
9	6 8	mpbir	$⊢ Rel recs (F)$