frrlem15

Description: Lemma for general well-founded recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023)

	Ref	Expression
Hypotheses	frrlem15.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)}))\}$
	frrlem15.2	$⊢ F = frecs (R, A, G)$
Assertion	frrlem15	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$

Proof

Step	Hyp	Ref	Expression
1		frrlem15.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		frrlem15.2	$⊢ F = frecs (R, A, G)$
3		vex	$⊢ x \in V$
4		vex	$⊢ u \in V$
5	3 4	breldm	$⊢ x g u \to x \in dom g$
6	5	adantr	$⊢ (x g u \land x h v) \to x \in dom g$
7		vex	$⊢ v \in V$
8	3 7	breldm	$⊢ x h v \to x \in dom h$
9	8	adantl	$⊢ (x g u \land x h v) \to x \in dom h$
10	6 9	elind	$⊢ (x g u \land x h v) \to x \in (dom g \cap dom h)$
11		id	$⊢ (x g u \land x h v) \to (x g u \land x h v)$
12	4	brresi	$⊢ x ({g ↾}_{(dom g \cap dom h)}) u \leftrightarrow (x \in (dom g \cap dom h) \land x g u)$
13	7	brresi	$⊢ x ({h ↾}_{(dom g \cap dom h)}) v \leftrightarrow (x \in (dom g \cap dom h) \land x h v)$
14	12 13	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))$
15		an4	$⊢ ((x \in (dom g \cap dom h) \land x g u) \land (x \in (dom g \cap dom h) \land x h v)) \leftrightarrow ((x \in (dom g \cap dom h) \land x \in (dom g \cap dom h)) \land (x g u \land x h v))$
16	14 15	bitri	$⊢ (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 \in (dom g \cap dom h)) \land (x g u \land x h v))$
17	10 10 11 16	syl21anbrc	$⊢ (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		inss1	$⊢ dom g \cap dom h \subseteq dom g$
19	1	frrlem3	$⊢ g \in B \to dom g \subseteq A$
20	18 19	sstrid	$⊢ g \in B \to dom g \cap dom h \subseteq A$
21	20	ad2antrl	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to dom g \cap dom h \subseteq A$
22		simpll	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to R Fr A$
23		frss	$⊢ dom g \cap dom h \subseteq A \to (R Fr A \to R Fr (dom g \cap dom h))$
24	21 22 23	sylc	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to R Fr (dom g \cap dom h)$
25		simplr	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to R Se A$
26		sess2	$⊢ dom g \cap dom h \subseteq A \to (R Se A \to R Se (dom g \cap dom h))$
27	21 25 26	sylc	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to R Se (dom g \cap dom h)$
28	1	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)}))$
29	28	adantl	$⊢ ((R Fr A \land R Se A) \land (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)}))$
30	1	frrlem4	$⊢ (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) = a G ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}))$
31		incom	$⊢ dom g \cap dom h = dom h \cap dom g$
32	31	reseq2i	$⊢ {h ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom h \cap dom g)}$
33		fneq12	$⊢ ({h ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom h \cap dom g)} \land dom g \cap dom h = dom h \cap dom g) \to (({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))$
34	32 31 33	mp2an	$⊢ ({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	32	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	31 36	ax-mp	$⊢ Pred (R, (dom g \cap dom h), a) = Pred (R, (dom h \cap dom g), a)$
38	32 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	oveq2i	$⊢ a G ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) = a G ({({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) = a G ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}) \leftrightarrow ({h ↾}_{(dom h \cap dom g)}) (a) = a G ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)})$
41	31 40	raleqbii	$⊢ \forall a \in (dom g \cap dom h) ({h ↾}_{(dom g \cap dom h)}) (a) = a G ({({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) = a G ({({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) = a G ({({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) = a G ({({h ↾}_{(dom h \cap dom g)}) ↾}_{Pred (R, (dom h \cap dom g), a)}))$
43	30 42	sylibr	$⊢ (h \in B \land g \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) = a G ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$
44	43	ancoms	$⊢ (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) = a G ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$
45	44	adantl	$⊢ ((R Fr A \land R Se A) \land (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) = a G ({({h ↾}_{(dom g \cap dom h)}) ↾}_{Pred (R, (dom g \cap dom h), a)}))$
46		frr3g	$⊢ ((R Fr (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) = a G ({({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) = a G ({({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)}$
47	24 27 29 45 46	syl211anc	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to {g ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom g \cap dom h)}$
48	47	breqd	$⊢ ((R Fr A \land R Se A) \land (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)$
49	48	biimprd	$⊢ ((R Fr A \land R Se A) \land (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)$
50	1	frrlem2	$⊢ g \in B \to Fun g$
51	50	funresd	$⊢ g \in B \to Fun ({g ↾}_{(dom g \cap dom h)})$
52	51	ad2antrl	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to Fun ({g ↾}_{(dom g \cap dom h)})$
53		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))$
54		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)$
55	54	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)$
56	53 55	simplbiim	$⊢ Fun ({g ↾}_{(dom g \cap dom h)}) \to ((x ({g ↾}_{(dom g \cap dom h)}) u \land x ({g ↾}_{(dom g \cap dom h)}) v) \to u = v)$
57	52 56	syl	$⊢ ((R Fr A \land R Se A) \land (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)$
58	49 57	sylan2d	$⊢ ((R Fr A \land R Se A) \land (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)$
59	17 58	syl5	$⊢ ((R Fr A \land R Se A) \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$

Metamath Proof Explorer

Theorem frrlem15

Proof