frrlem4

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012)

		Ref	Expression
	Hypothesis	frrlem4.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)}))\}$
	Assertion	frrlem4	$⊢ (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) = a G ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$

Proof

Step	Hyp	Ref	Expression
1		frrlem4.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	1	frrlem2	$⊢ 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	frrlem1	$⊢ 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) = a G ({g ↾}_{Pred (R, A, a)}))\}$
8	7	eqabri	$⊢ 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) = a G ({g ↾}_{Pred (R, A, a)}))$
9		fndm	$⊢ g Fn b \to dom g = b$
10	9	adantr	$⊢ (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b)) \to dom g = b$
11	10	raleqdv	$⊢ (g Fn b \land (b \subseteq A \land \forall a \in b Pred (R, A, a) \subseteq b)) \to (\forall a \in dom g g (a) = a G ({g ↾}_{Pred (R, A, a)}) \leftrightarrow \forall a \in b g (a) = a G ({g ↾}_{Pred (R, A, a)}))$
12	11	biimp3ar	$⊢ (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) = a G ({g ↾}_{Pred (R, A, a)})) \to \forall a \in dom g g (a) = a G ({g ↾}_{Pred (R, A, a)})$
13		rsp	$⊢ \forall a \in dom g g (a) = a G ({g ↾}_{Pred (R, A, a)}) \to (a \in dom g \to g (a) = a G ({g ↾}_{Pred (R, A, a)}))$
14	12 13	syl	$⊢ (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) = a G ({g ↾}_{Pred (R, A, a)})) \to (a \in dom g \to g (a) = a G ({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) = a G ({g ↾}_{Pred (R, A, a)})) \to (a \in dom g \to g (a) = a G ({g ↾}_{Pred (R, A, a)}))$
16	8 15	sylbi	$⊢ g \in B \to (a \in dom g \to g (a) = a G ({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) = a G ({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) = a G ({g ↾}_{Pred (R, A, a)})$
20		simpr	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to a \in (dom g \cap dom h)$
21	20	fvresd	$⊢ ((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	frrlem1	$⊢ 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) = a G ({h ↾}_{Pred (R, A, a)}))\}$
27	26	eqabri	$⊢ 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) = a G ({h ↾}_{Pred (R, A, a)}))$
28		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) = a G ({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) = a G ({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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)})))$
29		inss1	$⊢ b \cap c \subseteq b$
30		simpl2l	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to b \subseteq A$
31	29 30	sstrid	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to b \cap c \subseteq A$
32		simp2r	$⊢ (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) = a G ({g ↾}_{Pred (R, A, a)})) \to \forall a \in b Pred (R, A, a) \subseteq b$
33		simp2r	$⊢ (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) = a G ({h ↾}_{Pred (R, A, a)})) \to \forall a \in c Pred (R, A, a) \subseteq c$
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	32 33 47	syl2an	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c$
49		simpl1	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to g Fn b$
50	49	fndmd	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to dom g = b$
51		simpr1	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to h Fn c$
52	51	fndmd	$⊢ ((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) = a G ({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) = a G ({h ↾}_{Pred (R, A, a)}))) \to dom h = c$
53		ineq12	$⊢ (dom g = b \land dom h = c) \to dom g \cap dom h = b \cap c$
54	53	sseq1d	$⊢ (dom g = b \land dom h = c) \to (dom g \cap dom h \subseteq A \leftrightarrow b \cap c \subseteq A)$
55	53	sseq2d	$⊢ (dom g = b \land dom h = c) \to (Pred (R, A, a) \subseteq dom g \cap dom h \leftrightarrow Pred (R, A, a) \subseteq b \cap c)$
56	53 55	raleqbidv	$⊢ (dom g = b \land dom h = 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)$
57	54 56	anbi12d	$⊢ (dom g = b \land dom h = 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))$
58	50 52 57	syl2anc	$⊢ ((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) = a G ({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) = a G ({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) \leftrightarrow (b \cap c \subseteq A \land \forall a \in (b \cap c) Pred (R, A, a) \subseteq b \cap c))$
59	31 48 58	mpbir2and	$⊢ ((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) = a G ({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) = a G ({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)$
60	59	exlimivv	$⊢ \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) = a G ({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) = a G ({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	28 60	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) = a G ({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) = a G ({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	8 27 61	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)$
63	62	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)$
64		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))$
65	63 20 64	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)$
66	25 65	eqtrid	$⊢ ((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)$
67	66	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)}$
68	22 67	eqtrid	$⊢ ((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)}$
69	68	oveq2d	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to a G ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) = a G ({g ↾}_{Pred (R, A, a)})$
70	19 21 69	3eqtr4d	$⊢ ((g \in B \land h \in B) \land a \in (dom g \cap dom h)) \to ({g ↾}_{(dom g \cap dom h)}) (a) = a G ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)})$
71	70	ralrimiva	$⊢ (g \in B \land h \in B) \to \forall a \in (dom g \cap dom h) ({g ↾}_{(dom g \cap dom h)}) (a) = a G ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)})$
72	6 71	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) = a G ({({g ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$

Metamath Proof Explorer

Theorem frrlem4

Proof