wfrlem5

Description: Lemma for well-founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrlem5.1	$⊢ R We A$
	wfrlem5.2	$⊢ R Se A$
	wfrlem5.3	$⊢ 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	wfrlem5	$⊢ (g \in B \land h \in B) \to ((x g u \land x h v) \to u = v)$

Proof

Step	Hyp	Ref	Expression
1		wfrlem5.1	$⊢ R We A$
2		wfrlem5.2	$⊢ R Se A$
3		wfrlem5.3	$⊢ 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)}))\}$
4		vex	$⊢ x \in V$
5		vex	$⊢ u \in V$
6	4 5	breldm	$⊢ x g u \to x \in dom g$
7		vex	$⊢ v \in V$
8	4 7	breldm	$⊢ x h v \to x \in dom h$
9	6 8	anim12i	$⊢ (x g u \land x h v) \to (x \in dom g \land x \in dom h)$
10		elin	$⊢ x \in (dom g \cap dom h) \leftrightarrow (x \in dom g \land x \in dom h)$
11	9 10	sylibr	$⊢ (x g u \land x h v) \to x \in (dom g \cap dom h)$
12		anandi	$⊢ (x \in (dom g \cap dom h) \land (x g u \land x h v)) \leftrightarrow ((x \in (dom g \cap dom h) \land x g u) \land (x \in (dom g \cap dom h) \land x h v))$
13	5	brresi	$⊢ x ({g ↾}_{(dom g \cap dom h)}) u \leftrightarrow (x \in (dom g \cap dom h) \land x g u)$
14	7	brresi	$⊢ x ({h ↾}_{(dom g \cap dom h)}) v \leftrightarrow (x \in (dom g \cap dom h) \land x h v)$
15	13 14	anbi12i	$⊢ (x ({g ↾}_{(dom g \cap dom h)}) u \land x ({h ↾}_{(dom g \cap dom h)}) v) \leftrightarrow ((x \in (dom g \cap dom h) \land x g u) \land (x \in (dom g \cap dom h) \land x h v))$
16	12 15	sylbb2	$⊢ (x \in (dom g \cap dom h) \land (x g u \land x h v)) \to (x ({g ↾}_{(dom g \cap dom h)}) u \land x ({h ↾}_{(dom g \cap dom h)}) v)$
17	11 16	mpancom	$⊢ (x g u \land x h v) \to (x ({g ↾}_{(dom g \cap dom h)}) u \land x ({h ↾}_{(dom g \cap dom h)}) v)$
18	3	wfrlem3	$⊢ g \in B \to dom g \subseteq A$
19		ssinss1	$⊢ dom g \subseteq A \to dom g \cap dom h \subseteq A$
20		wess	$⊢ dom g \cap dom h \subseteq A \to (R We A \to R We (dom g \cap dom h))$
21	1 20	mpi	$⊢ dom g \cap dom h \subseteq A \to R We (dom g \cap dom h)$
22		sess2	$⊢ dom g \cap dom h \subseteq A \to (R Se A \to R Se (dom g \cap dom h))$
23	2 22	mpi	$⊢ dom g \cap dom h \subseteq A \to R Se (dom g \cap dom h)$
24	21 23	jca	$⊢ dom g \cap dom h \subseteq A \to (R We (dom g \cap dom h) \land R Se (dom g \cap dom h))$
25	18 19 24	3syl	$⊢ g \in B \to (R We (dom g \cap dom h) \land R Se (dom g \cap dom h))$
26	25	adantr	$⊢ (g \in B \land h \in B) \to (R We (dom g \cap dom h) \land R Se (dom g \cap dom h))$
27	3	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)}))$
28	3	wfrlem4	$⊢ (h \in B \land g \in B) \to (({h ↾}_{(dom h \cap dom g)}) Fn (dom h \cap dom g) \land \forall a \in (dom h \cap dom g) ({h ↾}_{(dom h \cap dom g)}) (a) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}))$
29	28	ancoms	$⊢ (g \in B \land h \in B) \to (({h ↾}_{(dom h \cap dom g)}) Fn (dom h \cap dom g) \land \forall a \in (dom h \cap dom g) ({h ↾}_{(dom h \cap dom g)}) (a) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}))$
30		incom	$⊢ dom g \cap dom h = dom h \cap dom g$
31	30	reseq2i	$⊢ {h ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom h \cap dom g)}$
32	31	fneq1i	$⊢ ({h ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \leftrightarrow ({h ↾}_{(dom h \cap dom g)}) Fn (dom g \cap dom h)$
33	30	fneq2i	$⊢ ({h ↾}_{(dom h \cap dom g)}) Fn (dom g \cap dom h) \leftrightarrow ({h ↾}_{(dom h \cap dom g)}) Fn (dom h \cap dom g)$
34	32 33	bitri	$⊢ ({h ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \leftrightarrow ({h ↾}_{(dom h \cap dom g)}) Fn (dom h \cap dom g)$
35	31	fveq1i	$⊢ ({h ↾}_{(dom g \cap dom h)}) (a) = ({h ↾}_{(dom h \cap dom g)}) (a)$
36		predeq2	$⊢ dom g \cap dom h = dom h \cap dom g \to Pred (R, (dom g \cap dom h), a) = Pred (R, (dom h \cap dom g), a)$
37	30 36	ax-mp	$⊢ Pred (R, (dom g \cap dom h), a) = Pred (R, (dom h \cap dom g), a)$
38	31 37	reseq12i	$⊢ {({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)} = {({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}$
39	38	fveq2i	$⊢ F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)})$
40	35 39	eqeq12i	$⊢ ({h ↾}_{(dom g \cap dom h)}) (a) = F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) \leftrightarrow ({h ↾}_{(dom h \cap dom g)}) (a) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)})$
41	30 40	raleqbii	$⊢ \forall a \in (dom g \cap dom h) ({h ↾}_{(dom g \cap dom h)}) (a) = F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) \leftrightarrow \forall a \in (dom h \cap dom g) ({h ↾}_{(dom h \cap dom g)}) (a) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)})$
42	34 41	anbi12i	$⊢ (({h ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \land \forall a \in (dom g \cap dom h) ({h ↾}_{(dom g \cap dom h)}) (a) = F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)})) \leftrightarrow (({h ↾}_{(dom h \cap dom g)}) Fn (dom h \cap dom g) \land \forall a \in (dom h \cap dom g) ({h ↾}_{(dom h \cap dom g)}) (a) = F ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}))$
43	29 42	sylibr	$⊢ (g \in B \land h \in B) \to (({h ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \land \forall a \in (dom g \cap dom h) ({h ↾}_{(dom g \cap dom h)}) (a) = F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$
44		wfr3g	$⊢ ((R We (dom g \cap dom h) \land R Se (dom g \cap dom h)) \land (({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)})) \land (({h ↾}_{(dom g \cap dom h)}) Fn (dom g \cap dom h) \land \forall a \in (dom g \cap dom h) ({h ↾}_{(dom g \cap dom h)}) (a) = F ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))) \to {g ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom g \cap dom h)}$
45	26 27 43 44	syl3anc	$⊢ (g \in B \land h \in B) \to {g ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom g \cap dom h)}$
46	45	breqd	$⊢ (g \in B \land h \in B) \to (x ({g ↾}_{(dom g \cap dom h)}) v \leftrightarrow x ({h ↾}_{(dom g \cap dom h)}) v)$
47	46	biimprd	$⊢ (g \in B \land h \in B) \to (x ({h ↾}_{(dom g \cap dom h)}) v \to x ({g ↾}_{(dom g \cap dom h)}) v)$
48	3	wfrlem2	$⊢ g \in B \to Fun g$
49		funres	$⊢ Fun g \to Fun ({g ↾}_{(dom g \cap dom h)})$
50		dffun2	$⊢ Fun ({g ↾}_{(dom g \cap dom h)}) \leftrightarrow (Rel ({g ↾}_{(dom g \cap dom h)}) \land \forall x \forall u \forall v ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v))$
51	50	simprbi	$⊢ Fun ({g ↾}_{(dom g \cap dom h)}) \to \forall x \forall u \forall v ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
52		2sp	$⊢ \forall u \forall v ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v) \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
53	52	sps	$⊢ \forall x \forall u \forall v ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v) \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
54	48 49 51 53	4syl	$⊢ g \in B \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
55	54	adantr	$⊢ (g \in B \land h \in B) \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
56	47 55	sylan2d	$⊢ (g \in B \land h \in B) \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({h ↾}_{(dom g \cap dom h)}) v) \to u = v)$
57	17 56	syl5	$⊢ (g \in B \land h \in B) \to ((x g u \land x h v) \to u = v)$

Metamath Proof Explorer

Theorem wfrlem5

Proof