bnj1326

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1326.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1326.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1326.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1326.4	$⊢ D = dom g \cap dom h$
Assertion	bnj1326	$⊢ (R FrSe A \land g \in C \land h \in C) \to {g ↾}_{D} = {h ↾}_{D}$

Proof

Step	Hyp	Ref	Expression
1		bnj1326.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1326.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1326.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1326.4	$⊢ D = dom g \cap dom h$
5		eleq1w	$⊢ q = h \to (q \in C \leftrightarrow h \in C)$
6	5	3anbi3d	$⊢ q = h \to ((R FrSe A \land g \in C \land q \in C) \leftrightarrow (R FrSe A \land g \in C \land h \in C))$
7		dmeq	$⊢ q = h \to dom q = dom h$
8	7	ineq2d	$⊢ q = h \to dom g \cap dom q = dom g \cap dom h$
9	8	reseq2d	$⊢ q = h \to {g ↾}_{(dom g \cap dom q)} = {g ↾}_{(dom g \cap dom h)}$
10	4	reseq2i	$⊢ {g ↾}_{D} = {g ↾}_{(dom g \cap dom h)}$
11	9 10	eqtr4di	$⊢ q = h \to {g ↾}_{(dom g \cap dom q)} = {g ↾}_{D}$
12	8	reseq2d	$⊢ q = h \to {q ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom h)}$
13		reseq1	$⊢ q = h \to {q ↾}_{(dom g \cap dom h)} = {h ↾}_{(dom g \cap dom h)}$
14	12 13	eqtrd	$⊢ q = h \to {q ↾}_{(dom g \cap dom q)} = {h ↾}_{(dom g \cap dom h)}$
15	4	reseq2i	$⊢ {h ↾}_{D} = {h ↾}_{(dom g \cap dom h)}$
16	14 15	eqtr4di	$⊢ q = h \to {q ↾}_{(dom g \cap dom q)} = {h ↾}_{D}$
17	11 16	eqeq12d	$⊢ q = h \to ({g ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom q)} \leftrightarrow {g ↾}_{D} = {h ↾}_{D})$
18	6 17	imbi12d	$⊢ q = h \to (((R FrSe A \land g \in C \land q \in C) \to {g ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom q)}) \leftrightarrow ((R FrSe A \land g \in C \land h \in C) \to {g ↾}_{D} = {h ↾}_{D}))$
19		eleq1w	$⊢ p = g \to (p \in C \leftrightarrow g \in C)$
20	19	3anbi2d	$⊢ p = g \to ((R FrSe A \land p \in C \land q \in C) \leftrightarrow (R FrSe A \land g \in C \land q \in C))$
21		dmeq	$⊢ p = g \to dom p = dom g$
22	21	ineq1d	$⊢ p = g \to dom p \cap dom q = dom g \cap dom q$
23	22	reseq2d	$⊢ p = g \to {p ↾}_{(dom p \cap dom q)} = {p ↾}_{(dom g \cap dom q)}$
24		reseq1	$⊢ p = g \to {p ↾}_{(dom g \cap dom q)} = {g ↾}_{(dom g \cap dom q)}$
25	23 24	eqtrd	$⊢ p = g \to {p ↾}_{(dom p \cap dom q)} = {g ↾}_{(dom g \cap dom q)}$
26	22	reseq2d	$⊢ p = g \to {q ↾}_{(dom p \cap dom q)} = {q ↾}_{(dom g \cap dom q)}$
27	25 26	eqeq12d	$⊢ p = g \to ({p ↾}_{(dom p \cap dom q)} = {q ↾}_{(dom p \cap dom q)} \leftrightarrow {g ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom q)})$
28	20 27	imbi12d	$⊢ p = g \to (((R FrSe A \land p \in C \land q \in C) \to {p ↾}_{(dom p \cap dom q)} = {q ↾}_{(dom p \cap dom q)}) \leftrightarrow ((R FrSe A \land g \in C \land q \in C) \to {g ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom q)}))$
29		eqid	$⊢ dom p \cap dom q = dom p \cap dom q$
30	1 2 3 29	bnj1311	$⊢ (R FrSe A \land p \in C \land q \in C) \to {p ↾}_{(dom p \cap dom q)} = {q ↾}_{(dom p \cap dom q)}$
31	28 30	chvarvv	$⊢ (R FrSe A \land g \in C \land q \in C) \to {g ↾}_{(dom g \cap dom q)} = {q ↾}_{(dom g \cap dom q)}$
32	18 31	chvarvv	$⊢ (R FrSe A \land g \in C \land h \in C) \to {g ↾}_{D} = {h ↾}_{D}$

Metamath Proof Explorer

Theorem bnj1326

Proof