fprlem1

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

	Ref	Expression
Hypotheses	fprlem.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)}))\}$
	fprlem.2	$⊢ F = frecs (R, A, G)$
Assertion	fprlem1	$⊢ ((R Fr A \land R Po 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		fprlem.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		fprlem.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		vex	$⊢ v \in V$
7	3 6	breldm	$⊢ x h v \to x \in dom h$
8		elin	$⊢ x \in (dom g \cap dom h) \leftrightarrow (x \in dom g \land x \in dom h)$
9	8	biimpri	$⊢ (x \in dom g \land x \in dom h) \to x \in (dom g \cap dom h)$
10	5 7 9	syl2an	$⊢ (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	6	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		inss2	$⊢ dom g \cap dom h \subseteq dom h$
19	1	frrlem3	$⊢ h \in B \to dom h \subseteq A$
20	18 19	sstrid	$⊢ h \in B \to dom g \cap dom h \subseteq A$
21	20	adantl	$⊢ (g \in B \land h \in B) \to dom g \cap dom h \subseteq A$
22	21	adantl	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to dom g \cap dom h \subseteq A$
23		simpl1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Fr A$
24		frss	$⊢ dom g \cap dom h \subseteq A \to (R Fr A \to R Fr (dom g \cap dom h))$
25	22 23 24	sylc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Fr (dom g \cap dom h)$
26		simpl2	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Po A$
27		poss	$⊢ dom g \cap dom h \subseteq A \to (R Po A \to R Po (dom g \cap dom h))$
28	22 26 27	sylc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Po (dom g \cap dom h)$
29		simpl3	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Se A$
30		sess2	$⊢ dom g \cap dom h \subseteq A \to (R Se A \to R Se (dom g \cap dom h))$
31	22 29 30	sylc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to R Se (dom g \cap dom h)$
32	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)}))$
33	32	adantl	$⊢ ((R Fr A \land R Po 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)}))$
34	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)}))$
35		incom	$⊢ dom g \cap dom h = dom h \cap dom g$
36	35	reseq2i	$⊢ {h ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom h \cap dom g)}$
37		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))$
38	36 35 37	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)$
39	36	fveq1i	$⊢ ({h ↾}_{(dom g \cap dom h)}) (a) = ({h ↾}_{(dom h \cap dom g)}) (a)$
40		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)$
41	35 40	ax-mp	$⊢ Pred (R, (dom g \cap dom h), a) = Pred (R, (dom h \cap dom g), a)$
42	36 41	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)}$
43	42	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)})$
44	39 43	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)})$
45	35 44	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)})$
46	38 45	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)}))$
47	34 46	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)}))$
48	47	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)}))$
49	48	adantl	$⊢ ((R Fr A \land R Po 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)}))$
50		fpr3g	$⊢ ((R Fr (dom g \cap dom h) \land R Po (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)}$
51	25 28 31 33 49 50	syl311anc	$⊢ ((R Fr A \land R Po 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)}$
52	51	breqd	$⊢ ((R Fr A \land R Po 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)$
53	52	biimprd	$⊢ ((R Fr A \land R Po 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)$
54	1	frrlem2	$⊢ g \in B \to Fun g$
55	54	ad2antrl	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in B \land h \in B)) \to Fun g$
56		funres	$⊢ Fun g \to Fun ({g ↾}_{(dom g \cap dom h)})$
57		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))$
58		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)$
59	58	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)$
60	57 59	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)$
61	55 56 60	3syl	$⊢ ((R Fr A \land R Po 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)$
62	53 61	sylan2d	$⊢ ((R Fr A \land R Po 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)$
63	17 62	syl5	$⊢ ((R Fr A \land R Po 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 fprlem1

Proof