fprresex

Description: The restriction of a function defined by well-founded recursion to the predecessor of an element of its domain is a set. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	fprfung.1	$⊢ F = frecs (R, A, G)$
	Assertion	fprresex	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to {F ↾}_{Pred (R, A, X)} \in V$

Proof

Step	Hyp	Ref	Expression
1		fprfung.1	$⊢ F = frecs (R, A, G)$
2	1	fprfung	$⊢ (R Fr A \land R Po A \land R Se A) \to Fun F$
3		funfvop	$⊢ (Fun F \land X \in dom F) \to ⟨X, F (X)⟩ \in F$
4	2 3	sylan	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to ⟨X, F (X)⟩ \in F$
5		df-frecs	$⊢ frecs (R, A, G) = ⋃ \{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)}))\}$
6	1 5	eqtri	$⊢ 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 G ({f ↾}_{Pred (R, A, y)}))\}$
7	6	eleq2i	$⊢ ⟨X, F (X)⟩ \in F \leftrightarrow ⟨X, F (X)⟩ \in ⋃ \{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)}))\}$
8		eluni	$⊢ ⟨X, F (X)⟩ \in ⋃ \{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)}))\} \leftrightarrow \exists g (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})$
9	7 8	bitri	$⊢ ⟨X, F (X)⟩ \in F \leftrightarrow \exists g (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})$
10	4 9	sylib	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to \exists g (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})$
11		eqid	$⊢ \{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)}))\} = \{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)}))\}$
12	11	frrlem1	$⊢ \{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)}))\}$
13	12	abeq2i	$⊢ g \in \{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)}))\} \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)}))$
14	13	biimpi	$⊢ g \in \{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)}))\} \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) = w G ({g ↾}_{Pred (R, A, w)}))$
15	14	adantl	$⊢ (⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \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) = w G ({g ↾}_{Pred (R, A, w)}))$
16	15	adantl	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})) \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) = w G ({g ↾}_{Pred (R, A, w)}))$
17		3simpa	$⊢ (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)})) \to (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z))$
18	2	ad2antrr	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to Fun F$
19		simprlr	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g \in \{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)}))\}$
20		elssuni	$⊢ g \in \{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)}))\} \to g \subseteq ⋃ \{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)}))\}$
21	19 20	syl	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g \subseteq ⋃ \{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)}))\}$
22	21 6	sseqtrrdi	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g \subseteq F$
23		predeq3	$⊢ w = X \to Pred (R, A, w) = Pred (R, A, X)$
24	23	sseq1d	$⊢ w = X \to (Pred (R, A, w) \subseteq z \leftrightarrow Pred (R, A, X) \subseteq z)$
25		simprrr	$⊢ ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z))) \to \forall w \in z Pred (R, A, w) \subseteq z$
26	25	adantl	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to \forall w \in z Pred (R, A, w) \subseteq z$
27		simplr	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X \in dom F$
28		simprll	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to ⟨X, F (X)⟩ \in g$
29		df-br	$⊢ X g F (X) \leftrightarrow ⟨X, F (X)⟩ \in g$
30	28 29	sylibr	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X g F (X)$
31		fvex	$⊢ F (X) \in V$
32		breldmg	$⊢ (X \in dom F \land F (X) \in V \land X g F (X)) \to X \in dom g$
33	31 32	mp3an2	$⊢ (X \in dom F \land X g F (X)) \to X \in dom g$
34	27 30 33	syl2anc	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X \in dom g$
35		simprrl	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g Fn z$
36	35	fndmd	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to dom g = z$
37	34 36	eleqtrd	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X \in z$
38	24 26 37	rspcdva	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to Pred (R, A, X) \subseteq z$
39	38 36	sseqtrrd	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to Pred (R, A, X) \subseteq dom g$
40		fun2ssres	$⊢ (Fun F \land g \subseteq F \land Pred (R, A, X) \subseteq dom g) \to {F ↾}_{Pred (R, A, X)} = {g ↾}_{Pred (R, A, X)}$
41	18 22 39 40	syl3anc	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to {F ↾}_{Pred (R, A, X)} = {g ↾}_{Pred (R, A, X)}$
42		vex	$⊢ g \in V$
43	42	resex	$⊢ {g ↾}_{Pred (R, A, X)} \in V$
44	41 43	eqeltrdi	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land ((⟨X, F (X)⟩ \in g \land g \in \{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)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to {F ↾}_{Pred (R, A, X)} \in V$
45	44	expr	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})) \to ((g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)) \to {F ↾}_{Pred (R, A, X)} \in V)$
46	17 45	syl5	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})) \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) = w G ({g ↾}_{Pred (R, A, w)})) \to {F ↾}_{Pred (R, A, X)} \in V)$
47	46	exlimdv	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})) \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) = w G ({g ↾}_{Pred (R, A, w)})) \to {F ↾}_{Pred (R, A, X)} \in V)$
48	16 47	mpd	$⊢ (((R Fr A \land R Po A \land R Se A) \land X \in dom F) \land (⟨X, F (X)⟩ \in g \land g \in \{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)}))\})) \to {F ↾}_{Pred (R, A, X)} \in V$
49	10 48	exlimddv	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to {F ↾}_{Pred (R, A, X)} \in V$

Metamath Proof Explorer

Theorem fprresex

Proof