frecseq123

Description: Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

		Ref	Expression
	Assertion	frecseq123	$⊢ (R = S \land A = B \land F = G) \to frecs (R, A, F) = frecs (S, B, G)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (R = S \land A = B \land F = G) \to A = B$
2	1	sseq2d	$⊢ (R = S \land A = B \land F = G) \to (x \subseteq A \leftrightarrow x \subseteq B)$
3		equid	$⊢ y = y$
4		predeq123	$⊢ (R = S \land A = B \land y = y) \to Pred (R, A, y) = Pred (S, B, y)$
5	3 4	mp3an3	$⊢ (R = S \land A = B) \to Pred (R, A, y) = Pred (S, B, y)$
6	5	3adant3	$⊢ (R = S \land A = B \land F = G) \to Pred (R, A, y) = Pred (S, B, y)$
7	6	sseq1d	$⊢ (R = S \land A = B \land F = G) \to (Pred (R, A, y) \subseteq x \leftrightarrow Pred (S, B, y) \subseteq x)$
8	7	ralbidv	$⊢ (R = S \land A = B \land F = G) \to (\forall y \in x Pred (R, A, y) \subseteq x \leftrightarrow \forall y \in x Pred (S, B, y) \subseteq x)$
9	2 8	anbi12d	$⊢ (R = S \land A = B \land F = G) \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \leftrightarrow (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x))$
10		simp3	$⊢ (R = S \land A = B \land F = G) \to F = G$
11	10	oveqd	$⊢ (R = S \land A = B \land F = G) \to y F ({f ↾}_{Pred (R, A, y)}) = y G ({f ↾}_{Pred (R, A, y)})$
12	6	reseq2d	$⊢ (R = S \land A = B \land F = G) \to {f ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (S, B, y)}$
13	12	oveq2d	$⊢ (R = S \land A = B \land F = G) \to y G ({f ↾}_{Pred (R, A, y)}) = y G ({f ↾}_{Pred (S, B, y)})$
14	11 13	eqtrd	$⊢ (R = S \land A = B \land F = G) \to y F ({f ↾}_{Pred (R, A, y)}) = y G ({f ↾}_{Pred (S, B, y)})$
15	14	eqeq2d	$⊢ (R = S \land A = B \land F = G) \to (f (y) = y F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow f (y) = y G ({f ↾}_{Pred (S, B, y)}))$
16	15	ralbidv	$⊢ (R = S \land A = B \land F = G) \to (\forall y \in x f (y) = y F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)}))$
17	9 16	3anbi23d	$⊢ (R = S \land A = B \land 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 F ({f ↾}_{Pred (R, A, y)})) \leftrightarrow (f Fn x \land (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)})))$
18	17	exbidv	$⊢ (R = S \land A = B \land 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 F ({f ↾}_{Pred (R, A, y)})) \leftrightarrow \exists x (f Fn x \land (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)})))$
19	18	abbidv	$⊢ (R = S \land A = B \land F = G) \to \{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 F ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)}))\}$
20	19	unieqd	$⊢ (R = S \land A = B \land F = G) \to ⋃ \{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 F ({f ↾}_{Pred (R, A, y)}))\} = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)}))\}$
21		df-frecs	$⊢ frecs (R, A, F) = ⋃ \{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 F ({f ↾}_{Pred (R, A, y)}))\}$
22		df-frecs	$⊢ frecs (S, B, G) = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq B \land \forall y \in x Pred (S, B, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (S, B, y)}))\}$
23	20 21 22	3eqtr4g	$⊢ (R = S \land A = B \land F = G) \to frecs (R, A, F) = frecs (S, B, G)$

Metamath Proof Explorer

Theorem frecseq123

Proof