wfrlem4

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by AV, 18-Jul-2022)

		Ref	Expression
	Hypothesis	wfrlem4.2	$⊢ 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) = F ({f ↾}_{Pred (R, A, y)}))\}$
	Assertion	wfrlem4	$⊢ (g \in B \land h \in B) \to (({g ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \land \forall a \in (dom g \cap dom h) ({g ↾}_{(dom g \cap dom h)}) (a) = F ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$

Proof

Step	Hyp	Ref	Expression
1		wfrlem4.2	$⊢ 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) = F ({f ↾}_{Pred (R, A, y)}))\}$
2	1	wfrlem2	$⊢ g \in B \to Fun g$
3	2	funfnd	$⊢ g \in B \to g Fn dom g$
4		fnresin1	$⊢ g Fn dom g \to ({g ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h)$
5	3 4	syl	$⊢ g \in B \to ({g ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h)$
6	5	adantr	$⊢ (g \in B \land h \in B) \to ({g ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h)$
7	1	wfrlem1	$⊢ B = \{g \| \exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}))\}$
8	7	abeq2i	$⊢ g \in B \leftrightarrow \exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}))$
9		fndm	$⊢ g Fn b \to dom g = b$
10	9	raleqdv	$⊢ g Fn b \to (\forall a \in dom g g (a) = F ({g ↾}_{Pred (R, A, a)}) \leftrightarrow \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}))$
11	10	biimpar	$⊢ (g Fn b \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \to \forall a \in dom g g (a) = F ({g ↾}_{Pred (R, A, a)})$
12		rsp	$⊢ \forall a \in dom g g (a) = F ({g ↾}_{Pred (R, A, a)}) \to (a \in dom g \to g (a) = F ({g ↾}_{Pred (R, A, a)}))$
13	11 12	syl	$⊢ (g Fn b \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \to (a \in dom g \to g (a) = F ({g ↾}_{Pred (R, A, a)}))$
14	13	3adant2	$⊢ (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \to (a \in dom g \to g (a) = F ({g ↾}_{Pred (R, A, a)}))$
15	14	exlimiv	$⊢ \exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \to (a \in dom g \to g (a) = F ({g ↾}_{Pred (R, A, a)}))$
16	8 15	sylbi	$⊢ g \in B \to (a \in dom g \to g (a) = F ({g ↾}_{Pred (R, A, a)}))$
17		elinel1	$⊢ a \in (dom g \cap dom h) \to a \in dom g$
18	16 17	impel	$⊢ (g \in B \land a \in (dom g \cap dom h)) \to g (a) = F ({g ↾}_{Pred (R, A, a)})$
19	18	adantlr	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to g (a) = F ({g ↾}_{Pred (R, A, a)})$
20		fvres	$⊢ a \in (dom g \cap dom h) \to ({g ↾}_{(dom g \cap dom h)}) (a) = g (a)$
21	20	adantl	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to ({g ↾}_{(dom g \cap dom h)}) (a) = g (a)$
22		resres	$⊢ {({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)} = {g ↾}_{((dom g \cap dom h) \cap Pred (R, (dom g \cap dom h), a))}$
23		predss	$⊢ Pred (R, (dom g \cap dom h), a) \subseteq dom g \cap dom h$
24		sseqin2	$⊢ Pred (R, (dom g \cap dom h), a) \subseteq dom g \cap dom h \leftrightarrow (dom g \cap dom h) \cap Pred (R, (dom g \cap dom h), a) = Pred (R, (dom g \cap dom h), a)$
25	23 24	mpbi	$⊢ (dom g \cap dom h) \cap Pred (R, (dom g \cap dom h), a) = Pred (R, (dom g \cap dom h), a)$
26	1	wfrlem1	$⊢ B = \{h \| \exists c (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))\}$
27	26	abeq2i	$⊢ h \in B \leftrightarrow \exists c (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))$
28		3an6	$⊢ ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \land (\forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \leftrightarrow ((g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)})))$
29	28	2exbii	$⊢ \exists b \exists c ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \land (\forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \leftrightarrow \exists b \exists c ((g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)})))$
30		exdistrv	$⊢ \exists b \exists c ((g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \leftrightarrow (\exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land \exists c (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)})))$
31	29 30	bitri	$⊢ \exists b \exists c ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \land (\forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \leftrightarrow (\exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land \exists c (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)})))$
32		ssinss1	$⊢ b \subseteq A \to b \cap c \subseteq A$
33	32	ad2antrr	$⊢ ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to b \cap c \subseteq A$
34		nfra1	$⊢ Ⅎ a \forall a \in b Pred (R, A, a) \subseteq b$
35		nfra1	$⊢ Ⅎ a \forall a \in c Pred (R, A, a) \subseteq c$
36	34 35	nfan	$⊢ Ⅎ a (\forall a \in b Pred (R, A, a) \subseteq b \land \forall a \in c Pred (R, A, a) \subseteq c)$
37		elinel1	$⊢ a \in (b \cap c) \to a \in b$
38		rsp	$⊢ \forall a \in b Pred (R, A, a) \subseteq b \to (a \in b \to Pred (R, A, a) \subseteq b)$
39	37 38	syl5com	$⊢ a \in (b \cap c) \to (\forall a \in b Pred (R, A, a) \subseteq b \to Pred (R, A, a) \subseteq b)$
40		elinel2	$⊢ a \in (b \cap c) \to a \in c$
41		rsp	$⊢ \forall a \in c Pred (R, A, a) \subseteq c \to (a \in c \to Pred (R, A, a) \subseteq c)$
42	40 41	syl5com	$⊢ a \in (b \cap c) \to (\forall a \in c Pred (R, A, a) \subseteq c \to Pred (R, A, a) \subseteq c)$
43	39 42	anim12d	$⊢ a \in (b \cap c) \to ((\forall a \in b Pred (R, A, a) \subseteq b \land \forall a \in c Pred (R, A, a) \subseteq c) \to (Pred (R, A, a) \subseteq b \land Pred (R, A, a) \subseteq c))$
44		ssin	$⊢ (Pred (R, A, a) \subseteq b \land Pred (R, A, a) \subseteq c) \leftrightarrow Pred (R, A, a) \subseteq b \cap c$
45	44	biimpi	$⊢ (Pred (R, A, a) \subseteq b \land Pred (R, A, a) \subseteq c) \to Pred (R, A, a) \subseteq b \cap c$
46	43 45	syl6com	$⊢ (\forall a \in b Pred (R, A, a) \subseteq b \land \forall a \in c Pred (R, A, a) \subseteq c) \to (a \in (b \cap c) \to Pred (R, A, a) \subseteq b \cap c)$
47	36 46	ralrimi	$⊢ (\forall a \in b Pred (R, A, a) \subseteq b \land \forall a \in c Pred (R, A, a) \subseteq c) \to \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c$
48	47	ad2ant2l	$⊢ ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c$
49	33 48	jca	$⊢ ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (b \cap c \subseteq A \land \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c)$
50		fndm	$⊢ h Fn c \to dom h = c$
51	9 50	ineqan12d	$⊢ (g Fn b \land h Fn c) \to dom g \cap dom h = b \cap c$
52		sseq1	$⊢ dom g \cap dom h = b \cap c \to (dom g \cap dom h \subseteq A \leftrightarrow b \cap c \subseteq A)$
53		sseq2	$⊢ dom g \cap dom h = b \cap c \to (Pred (R, A, a) \subseteq dom g \cap dom h \leftrightarrow Pred (R, A, a) \subseteq b \cap c)$
54	53	raleqbi1dv	$⊢ dom g \cap dom h = b \cap c \to (\forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h \leftrightarrow \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c)$
55	52 54	anbi12d	$⊢ dom g \cap dom h = b \cap c \to ((dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h) \leftrightarrow (b \cap c \subseteq A \land \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c))$
56	55	imbi2d	$⊢ dom g \cap dom h = b \cap c \to ((((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)) \leftrightarrow (((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (b \cap c \subseteq A \land \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c)))$
57	51 56	syl	$⊢ (g Fn b \land h Fn c) \to ((((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)) \leftrightarrow (((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (b \cap c \subseteq A \land \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c)))$
58	49 57	mpbiri	$⊢ (g Fn b \land h Fn c) \to (((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h))$
59	58	imp	$⊢ ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c))) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
60	59	3adant3	$⊢ ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \land (\forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
61	60	exlimivv	$⊢ \exists b \exists c ((g Fn b \land h Fn c) \land ((b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c)) \land (\forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)}) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
62	31 61	sylbir	$⊢ (\exists b (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b) \land \forall a \in b g (a) = F ({g ↾}_{Pred (R, A, a)})) \land \exists c (h Fn c \land (c \subseteq A \land \forall a \in c Pred (R, A, a) \subseteq c) \land \forall a \in c h (a) = F ({h ↾}_{Pred (R, A, a)}))) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
63	8 27 62	syl2anb	$⊢ (g \in B \land h \in B) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
64	63	adantr	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h)$
65		simpr	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to a \in (dom g \cap dom h)$
66		preddowncl	$⊢ (dom g \cap dom h \subseteq A \land \forall a \in (dom g \cap dom h) Pred (R, A, a) \subseteq dom g \cap dom h) \to (a \in (dom g \cap dom h) \to Pred (R, (dom g \cap dom h), a) = Pred (R, A, a))$
67	64 65 66	sylc	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to Pred (R, (dom g \cap dom h), a) = Pred (R, A, a)$
68	25 67	syl5eq	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to (dom g \cap dom h) \cap Pred (R, (dom g \cap dom h), a) = Pred (R, A, a)$
69	68	reseq2d	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to {g ↾}_{((dom g \cap dom h) \cap Pred (R, (dom g \cap dom h), a))} = {g ↾}_{Pred (R, A, a)}$
70	22 69	syl5eq	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to {({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)} = {g ↾}_{Pred (R, A, a)}$
71	70	fveq2d	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to F ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) = F ({g ↾}_{Pred (R, A, a)})$
72	19 21 71	3eqtr4d	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to ({g ↾}_{(dom g \cap dom h)}) (a) = F ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)})$
73	72	ralrimiva	$⊢ (g \in B \land h \in B) \to \forall a \in (dom g \cap dom h) ({g ↾}_{(dom g \cap dom h)}) (a) = F ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)})$
74	6 73	jca	$⊢ (g \in B \land h \in B) \to (({g ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \land \forall a \in (dom g \cap dom h) ({g ↾}_{(dom g \cap dom h)}) (a) = F ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$

Metamath Proof Explorer

Theorem wfrlem4

Proof