frrlem3

Description: Lemma for well-founded recursion. An acceptable function's domain is a subset of A . (Contributed by Paul Chapman, 21-Apr-2012)

		Ref	Expression
	Hypothesis	frrlem1.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)}))\}$
	Assertion	frrlem3	$⊢ g \in B \to dom g \subseteq A$

Step	Hyp	Ref	Expression
1		frrlem1.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	1	frrlem1	$⊢ B = \{g \| \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)}))\}$
3	2	eqabri	$⊢ g \in B \leftrightarrow \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)}))$
4		fndm	$⊢ g Fn z \to dom g = z$
5	4	sseq1d	$⊢ g Fn z \to (dom g \subseteq A \leftrightarrow z \subseteq A)$
6	5	biimpar	$⊢ (g Fn z \land z \subseteq A) \to dom g \subseteq A$
7	6	adantrr	$⊢ (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)) \to dom g \subseteq A$
8	7	3adant3	$⊢ (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)})) \to dom g \subseteq A$
9	8	exlimiv	$⊢ \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)})) \to dom g \subseteq A$
10	3 9	sylbi	$⊢ g \in B \to dom g \subseteq A$

Metamath Proof Explorer