Metamath Proof Explorer

Theorem wfrlem3OLDa

Description: Lemma for well-ordered recursion. Show membership in the class of acceptable functions. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020)

		Ref	Expression
	Hypotheses	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)}))\}$
		wfrlem3OLDa.2	$⊢ G \in V$
	Assertion	wfrlem3OLDa	$⊢ 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)}))$

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		wfrlem3OLDa.2	$⊢ G \in V$
3		fneq1	$⊢ g = G \to (g Fn z \leftrightarrow G Fn z)$
4		fveq1	$⊢ g = G \to g (w) = G (w)$
5		reseq1	$⊢ g = G \to {g ↾}_{Pred (R, A, w)} = {G ↾}_{Pred (R, A, w)}$
6	5	fveq2d	$⊢ g = G \to F ({g ↾}_{Pred (R, A, w)}) = F ({G ↾}_{Pred (R, A, w)})$
7	4 6	eqeq12d	$⊢ g = G \to (g (w) = F ({g ↾}_{Pred (R, A, w)}) \leftrightarrow G (w) = F ({G ↾}_{Pred (R, A, w)}))$
8	7	ralbidv	$⊢ g = G \to (\forall w \in z g (w) = F ({g ↾}_{Pred (R, A, w)}) \leftrightarrow \forall w \in z G (w) = F ({G ↾}_{Pred (R, A, w)}))$
9	3 8	3anbi13d	$⊢ g = G \to ((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)})) \leftrightarrow (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)})))$
10	9	exbidv	$⊢ g = G \to (\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)})) \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)})))$
11	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)}))\}$
12	2 10 11	elab2	$⊢ 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)}))$