frrlem6

Description: Lemma for well-founded recursion. The well-founded recursion generator is a relation. (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	frrlem6	$⊢ Rel F$

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	1 2	frrlem5	$⊢ F = ⋃ B$
4	3	releqi	$⊢ Rel F \leftrightarrow Rel ⋃ B$
5		reluni	$⊢ Rel ⋃ B \leftrightarrow \forall g \in B Rel g$
6	4 5	bitri	$⊢ Rel F \leftrightarrow \forall g \in B Rel g$
7	1	frrlem2	$⊢ g \in B \to Fun g$
8		funrel	$⊢ Fun g \to Rel g$
9	7 8	syl	$⊢ g \in B \to Rel g$
10	6 9	mprgbir	$⊢ Rel F$

Metamath Proof Explorer