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

Metamath Proof Explorer

Theorem frrlem5

Description: Lemma for well-founded recursion. State the well-founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022)

		Ref	Expression
	Hypotheses	frrlem5.1	$⊢ B = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
		frrlem5.2	$⊢ F = frecs (R, A, G)$
	Assertion	frrlem5	$⊢ F = ⋃ B$

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	$⊢ B = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
2		frrlem5.2	$⊢ F = frecs (R, A, G)$
3		df-frecs	$⊢ frecs (R, A, G) = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
4	1	unieqi	$⊢ ⋃ B = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
5	3 2 4	3eqtr4i	$⊢ F = ⋃ B$