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	eqabri	$⊢ 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	bilani	$⊢ (⟨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)}))$
15	14	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)}))$
16		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))$
17	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$
18		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)}))\}$
19		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)}))\}$
20	18 19	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)}))\}$
21	20 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$
22		predeq3	$⊢ w = X \to Pred (R, A, w) = Pred (R, A, X)$
23	22	sseq1d	$⊢ w = X \to (Pred (R, A, w) \subseteq z \leftrightarrow Pred (R, A, X) \subseteq z)$
24		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$
25	24	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$
26		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$
27		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$
28		df-br	$⊢ X g F (X) \leftrightarrow ⟨X, F (X)⟩ \in g$
29	27 28	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)$
30		fvex	$⊢ F (X) \in V$
31		breldmg	$⊢ (X \in dom F \land F (X) \in V \land X g F (X)) \to X \in dom g$
32	30 31	mp3an2	$⊢ (X \in dom F \land X g F (X)) \to X \in dom g$
33	26 29 32	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$
34		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$
35	34	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$
36	33 35	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$
37	23 25 36	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$
38	37 35	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$
39		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)}$
40	17 21 38 39	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)}$
41		vex	$⊢ g \in V$
42	41	resex	$⊢ {g ↾}_{Pred (R, A, X)} \in V$
43	40 42	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$
44	43	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)$
45	16 44	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)$
46	45	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)$
47	15 46	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$
48	10 47	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