wfrlem1

Description: Lemma for well-founded recursion. The final item we are interested in is the union of acceptable functions B . This lemma just changes bound variables for later use. (Contributed by Scott Fenton, 21-Apr-2011)

		Ref	Expression
	Hypothesis	wfrlem1.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	wfrlem1	$⊢ 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)}))\}$

Proof

Step	Hyp	Ref	Expression
1		wfrlem1.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		fneq1	$⊢ f = g \to (f Fn x \leftrightarrow g Fn x)$
3		fveq1	$⊢ f = g \to f (y) = g (y)$
4		reseq1	$⊢ f = g \to {f ↾}_{Pred (R, A, y)} = {g ↾}_{Pred (R, A, y)}$
5	4	fveq2d	$⊢ f = g \to F ({f ↾}_{Pred (R, A, y)}) = F ({g ↾}_{Pred (R, A, y)})$
6	3 5	eqeq12d	$⊢ f = g \to (f (y) = F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow g (y) = F ({g ↾}_{Pred (R, A, y)}))$
7	6	ralbidv	$⊢ f = g \to (\forall y \in x f (y) = F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)}))$
8	2 7	3anbi13d	$⊢ f = g \to ((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)})) \leftrightarrow (g Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)})))$
9	8	exbidv	$⊢ f = g \to (\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)})) \leftrightarrow \exists x (g Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)})))$
10		fneq2	$⊢ x = z \to (g Fn x \leftrightarrow g Fn z)$
11		sseq1	$⊢ x = z \to (x \subseteq A \leftrightarrow z \subseteq A)$
12		sseq2	$⊢ x = z \to (Pred (R, A, y) \subseteq x \leftrightarrow Pred (R, A, y) \subseteq z)$
13	12	raleqbi1dv	$⊢ x = z \to (\forall y \in x Pred (R, A, y) \subseteq x \leftrightarrow \forall y \in z Pred (R, A, y) \subseteq z)$
14		predeq3	$⊢ y = w \to Pred (R, A, y) = Pred (R, A, w)$
15	14	sseq1d	$⊢ y = w \to (Pred (R, A, y) \subseteq z \leftrightarrow Pred (R, A, w) \subseteq z)$
16	15	cbvralvw	$⊢ \forall y \in z Pred (R, A, y) \subseteq z \leftrightarrow \forall w \in z Pred (R, A, w) \subseteq z$
17	13 16	syl6bb	$⊢ x = z \to (\forall y \in x Pred (R, A, y) \subseteq x \leftrightarrow \forall w \in z Pred (R, A, w) \subseteq z)$
18	11 17	anbi12d	$⊢ x = z \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \leftrightarrow (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z))$
19		raleq	$⊢ x = z \to (\forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in z g (y) = F ({g ↾}_{Pred (R, A, y)}))$
20		fveq2	$⊢ y = w \to g (y) = g (w)$
21	14	reseq2d	$⊢ y = w \to {g ↾}_{Pred (R, A, y)} = {g ↾}_{Pred (R, A, w)}$
22	21	fveq2d	$⊢ y = w \to F ({g ↾}_{Pred (R, A, y)}) = F ({g ↾}_{Pred (R, A, w)})$
23	20 22	eqeq12d	$⊢ y = w \to (g (y) = F ({g ↾}_{Pred (R, A, y)}) \leftrightarrow g (w) = F ({g ↾}_{Pred (R, A, w)}))$
24	23	cbvralvw	$⊢ \forall y \in z g (y) = F ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall w \in z g (w) = F ({g ↾}_{Pred (R, A, w)})$
25	19 24	syl6bb	$⊢ x = z \to (\forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall w \in z g (w) = F ({g ↾}_{Pred (R, A, w)}))$
26	10 18 25	3anbi123d	$⊢ x = z \to ((g Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)})) \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)})))$
27	26	cbvexvw	$⊢ \exists x (g Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x g (y) = F ({g ↾}_{Pred (R, A, y)})) \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)}))$
28	9 27	syl6bb	$⊢ f = g \to (\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)})) \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)})))$
29	28	cbvabv	$⊢ \{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)}))\} = \{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)}))\}$
30	1 29	eqtri	$⊢ 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)}))\}$

Metamath Proof Explorer

Theorem wfrlem1

Proof