Metamath Proof Explorer

Theorem wfrlem2OLD

Description: Lemma for well-ordered recursion. An acceptable function is a function. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

		Ref	Expression
	Hypothesis	wfrlem1OLD.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) = F ({f ↾}_{Pred (R, A, y)}))\}$
	Assertion	wfrlem2OLD	$⊢ g \in B \to Fun g$

Proof

Step	Hyp	Ref	Expression
1		wfrlem1OLD.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) = F ({f ↾}_{Pred (R, A, y)}))\}$
2	1	wfrlem1OLD	$⊢ 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) = F ({g ↾}_{Pred (R, A, w)}))\}$
3	2	abeq2i	$⊢ 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) = F ({g ↾}_{Pred (R, A, w)}))$
4		fnfun	$⊢ g Fn z \to Fun g$
5	4	3ad2ant1	$⊢ (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) = F ({g ↾}_{Pred (R, A, w)})) \to Fun g$
6	5	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) = F ({g ↾}_{Pred (R, A, w)})) \to Fun g$
7	3 6	sylbi	$⊢ g \in B \to Fun g$