frrlem10

Description: Lemma for well-founded recursion. Under the compatibility hypothesis, compute the value of F within its domain. (Contributed by Scott Fenton, 6-Dec-2022)

	Ref	Expression
Hypotheses	frrlem9.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)}))\}$
	frrlem9.2	$⊢ F = frecs (R, A, G)$
	frrlem9.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
Assertion	frrlem10	$⊢ (φ \land y \in dom F) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$

Proof

Step	Hyp	Ref	Expression
1		frrlem9.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		frrlem9.2	$⊢ F = frecs (R, A, G)$
3		frrlem9.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
4		vex	$⊢ y \in V$
5	4	eldm2	$⊢ y \in dom F \leftrightarrow \exists z ⟨y, z⟩ \in F$
6	1 2	frrlem5	$⊢ F = ⋃ B$
7	1	unieqi	$⊢ ⋃ 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)}))\}$
8	6 7	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)}))\}$
9	8	eleq2i	$⊢ ⟨y, z⟩ \in F \leftrightarrow ⟨y, z⟩ \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		eluniab	$⊢ ⟨y, z⟩ \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 f (⟨y, z⟩ \in f \land \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	9 10	bitri	$⊢ ⟨y, z⟩ \in F \leftrightarrow \exists f (⟨y, z⟩ \in f \land \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		19.8a	$⊢ (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 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)}))$
13	12	3ad2ant2	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \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)}))$
14		abid	$⊢ f \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 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)}))$
15	13 14	sylibr	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \to f \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)}))\}$
16		elssuni	$⊢ f \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 \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)}))\}$
17	15 16	syl	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \to f \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)}))\}$
18	17 8	sseqtrrdi	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \to f \subseteq F$
19		simpl23	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)})$
20		simpl3	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to ⟨y, z⟩ \in f$
21		vex	$⊢ z \in V$
22	4 21	opeldm	$⊢ ⟨y, z⟩ \in f \to y \in dom f$
23	20 22	syl	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to y \in dom f$
24		simpl21	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to f Fn x$
25	24	fndmd	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to dom f = x$
26	23 25	eleqtrd	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to y \in x$
27		rsp	$⊢ \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}) \to (y \in x \to f (y) = y G ({f ↾}_{Pred (R, A, y)}))$
28	19 26 27	sylc	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to f (y) = y G ({f ↾}_{Pred (R, A, y)})$
29		simpl1	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to φ$
30	1 2 3	frrlem9	$⊢ φ \to Fun F$
31	29 30	syl	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to Fun F$
32		simpr	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to f \subseteq F$
33		funssfv	$⊢ (Fun F \land f \subseteq F \land y \in dom f) \to F (y) = f (y)$
34	31 32 23 33	syl3anc	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to F (y) = f (y)$
35		simp22r	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \to \forall y \in x Pred (R, A, y) \subseteq x$
36	35	adantr	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to \forall y \in x Pred (R, A, y) \subseteq x$
37		rsp	$⊢ \forall y \in x Pred (R, A, y) \subseteq x \to (y \in x \to Pred (R, A, y) \subseteq x)$
38	36 26 37	sylc	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to Pred (R, A, y) \subseteq x$
39	38 25	sseqtrrd	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to Pred (R, A, y) \subseteq dom f$
40		fun2ssres	$⊢ (Fun F \land f \subseteq F \land Pred (R, A, y) \subseteq dom f) \to {F ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (R, A, y)}$
41	31 32 39 40	syl3anc	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to {F ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (R, A, y)}$
42	41	oveq2d	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to y G ({F ↾}_{Pred (R, A, y)}) = y G ({f ↾}_{Pred (R, A, y)})$
43	28 34 42	3eqtr4d	$⊢ ((φ \land (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 ⟨y, z⟩ \in f) \land f \subseteq F) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$
44	18 43	mpdan	$⊢ (φ \land (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 ⟨y, z⟩ \in f) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$
45	44	3exp	$⊢ φ \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)})) \to (⟨y, z⟩ \in f \to F (y) = y G ({F ↾}_{Pred (R, A, y)})))$
46	45	exlimdv	$⊢ φ \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)})) \to (⟨y, z⟩ \in f \to F (y) = y G ({F ↾}_{Pred (R, A, y)})))$
47	46	impcomd	$⊢ φ \to ((⟨y, z⟩ \in f \land \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 (y) = y G ({F ↾}_{Pred (R, A, y)}))$
48	47	exlimdv	$⊢ φ \to (\exists f (⟨y, z⟩ \in f \land \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 (y) = y G ({F ↾}_{Pred (R, A, y)}))$
49	11 48	syl5bi	$⊢ φ \to (⟨y, z⟩ \in F \to F (y) = y G ({F ↾}_{Pred (R, A, y)}))$
50	49	exlimdv	$⊢ φ \to (\exists z ⟨y, z⟩ \in F \to F (y) = y G ({F ↾}_{Pred (R, A, y)}))$
51	5 50	syl5bi	$⊢ φ \to (y \in dom F \to F (y) = y G ({F ↾}_{Pred (R, A, y)}))$
52	51	imp	$⊢ (φ \land y \in dom F) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$

Metamath Proof Explorer

Theorem frrlem10

Proof