wrecseq123

Description: General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	$⊢ A = B \to (x \subseteq A \leftrightarrow x \subseteq B)$
2	1	3ad2ant2	$⊢ (R = S \land A = B \land F = G) \to (x \subseteq A \leftrightarrow x \subseteq B)$
3		predeq1	$⊢ R = S \to Pred (R, A, y) = Pred (S, A, y)$
4		predeq2	$⊢ A = B \to Pred (S, A, y) = Pred (S, B, y)$
5	3 4	sylan9eq	$⊢ (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	5	reseq2d	$⊢ (R = S \land A = B) \to {f ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (S, B, y)}$
12	11	3adant3	$⊢ (R = S \land A = B \land F = G) \to {f ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (S, B, y)}$
13	10 12	fveq12d	$⊢ (R = S \land A = B \land F = G) \to F ({f ↾}_{Pred (R, A, y)}) = G ({f ↾}_{Pred (S, B, y)})$
14	13	eqeq2d	$⊢ (R = S \land A = B \land F = G) \to (f (y) = F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow f (y) = G ({f ↾}_{Pred (S, B, y)}))$
15	14	ralbidv	$⊢ (R = S \land A = B \land F = G) \to (\forall y \in x f (y) = F ({f ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in x f (y) = G ({f ↾}_{Pred (S, B, y)}))$
16	9 15	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) = 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) = G ({f ↾}_{Pred (S, B, y)})))$
17	16	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) = 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) = G ({f ↾}_{Pred (S, B, y)})))$
18	17	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) = 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) = G ({f ↾}_{Pred (S, B, y)}))\}$
19	18	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) = 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) = G ({f ↾}_{Pred (S, B, y)}))\}$
20		df-wrecs	$⊢ wrecs (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) = F ({f ↾}_{Pred (R, A, y)}))\}$
21		df-wrecs	$⊢ wrecs (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) = G ({f ↾}_{Pred (S, B, y)}))\}$
22	19 20 21	3eqtr4g	$⊢ (R = S \land A = B \land F = G) \to wrecs (R, A, F) = wrecs (S, B, G)$

Metamath Proof Explorer

Theorem wrecseq123

Proof