frrlem1

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 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	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)}))\}$

Proof

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		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	oveq2d	$⊢ f = g \to y G ({f ↾}_{Pred (R, A, y)}) = y G ({g ↾}_{Pred (R, A, y)})$
6	3 5	eqeq12d	$⊢ f = g \to (f (y) = y G ({f ↾}_{Pred (R, A, y)}) \leftrightarrow g (y) = y G ({g ↾}_{Pred (R, A, y)}))$
7	6	ralbidv	$⊢ f = g \to (\forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in x g (y) = y G ({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) = y G ({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) = y G ({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) = y G ({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) = y G ({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	bitrdi	$⊢ 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) = y G ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in z g (y) = y G ({g ↾}_{Pred (R, A, y)}))$
20		fveq2	$⊢ y = w \to g (y) = g (w)$
21		id	$⊢ y = w \to y = w$
22	14	reseq2d	$⊢ y = w \to {g ↾}_{Pred (R, A, y)} = {g ↾}_{Pred (R, A, w)}$
23	21 22	oveq12d	$⊢ y = w \to y G ({g ↾}_{Pred (R, A, y)}) = w G ({g ↾}_{Pred (R, A, w)})$
24	20 23	eqeq12d	$⊢ y = w \to (g (y) = y G ({g ↾}_{Pred (R, A, y)}) \leftrightarrow g (w) = w G ({g ↾}_{Pred (R, A, w)}))$
25	24	cbvralvw	$⊢ \forall y \in z g (y) = y G ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)})$
26	19 25	bitrdi	$⊢ x = z \to (\forall y \in x g (y) = y G ({g ↾}_{Pred (R, A, y)}) \leftrightarrow \forall w \in z g (w) = w G ({g ↾}_{Pred (R, A, w)}))$
27	10 18 26	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) = y G ({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) = w G ({g ↾}_{Pred (R, A, w)})))$
28	27	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) = y G ({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) = w G ({g ↾}_{Pred (R, A, w)}))$
29	9 28	bitrdi	$⊢ 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) = y G ({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) = w G ({g ↾}_{Pred (R, A, w)})))$
30	29	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) = y G ({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) = w G ({g ↾}_{Pred (R, A, w)}))\}$
31	1 30	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) = w G ({g ↾}_{Pred (R, A, w)}))\}$

Metamath Proof Explorer

Theorem frrlem1

Proof