bnj1280

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	bnj1280.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1280.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1280.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1280.4	$⊢ D = dom g \cap dom h$
	bnj1280.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
	bnj1280.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
	bnj1280.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
	bnj1280.17	$⊢ ψ \to pred (x, A, R) \cap E = \emptyset$
Assertion	bnj1280	$⊢ ψ \to {g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)}$

Proof

Step	Hyp	Ref	Expression
1		bnj1280.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1280.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1280.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1280.4	$⊢ D = dom g \cap dom h$
5		bnj1280.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
6		bnj1280.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
7		bnj1280.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
8		bnj1280.17	$⊢ ψ \to pred (x, A, R) \cap E = \emptyset$
9	1 2 3 4 5 6 7	bnj1286	$⊢ ψ \to pred (x, A, R) \subseteq D$
10	9	sseld	$⊢ ψ \to (z \in pred (x, A, R) \to z \in D)$
11		disj1	$⊢ pred (x, A, R) \cap E = \emptyset \leftrightarrow \forall z (z \in pred (x, A, R) \to \neg z \in E)$
12	8 11	sylib	$⊢ ψ \to \forall z (z \in pred (x, A, R) \to \neg z \in E)$
13	12	19.21bi	$⊢ ψ \to (z \in pred (x, A, R) \to \neg z \in E)$
14		fveq2	$⊢ x = z \to g (x) = g (z)$
15		fveq2	$⊢ x = z \to h (x) = h (z)$
16	14 15	neeq12d	$⊢ x = z \to (g (x) \neq h (x) \leftrightarrow g (z) \neq h (z))$
17	16 5	elrab2	$⊢ z \in E \leftrightarrow (z \in D \land g (z) \neq h (z))$
18	17	notbii	$⊢ \neg z \in E \leftrightarrow \neg (z \in D \land g (z) \neq h (z))$
19		imnan	$⊢ (z \in D \to \neg g (z) \neq h (z)) \leftrightarrow \neg (z \in D \land g (z) \neq h (z))$
20		nne	$⊢ \neg g (z) \neq h (z) \leftrightarrow g (z) = h (z)$
21	20	imbi2i	$⊢ (z \in D \to \neg g (z) \neq h (z)) \leftrightarrow (z \in D \to g (z) = h (z))$
22	18 19 21	3bitr2i	$⊢ \neg z \in E \leftrightarrow (z \in D \to g (z) = h (z))$
23	13 22	imbitrdi	$⊢ ψ \to (z \in pred (x, A, R) \to (z \in D \to g (z) = h (z)))$
24	10 23	mpdd	$⊢ ψ \to (z \in pred (x, A, R) \to g (z) = h (z))$
25	24	imp	$⊢ (ψ \land z \in pred (x, A, R)) \to g (z) = h (z)$
26		fvres	$⊢ z \in D \to ({g ↾}_{D}) (z) = g (z)$
27	10 26	syl6	$⊢ ψ \to (z \in pred (x, A, R) \to ({g ↾}_{D}) (z) = g (z))$
28	27	imp	$⊢ (ψ \land z \in pred (x, A, R)) \to ({g ↾}_{D}) (z) = g (z)$
29		fvres	$⊢ z \in D \to ({h ↾}_{D}) (z) = h (z)$
30	10 29	syl6	$⊢ ψ \to (z \in pred (x, A, R) \to ({h ↾}_{D}) (z) = h (z))$
31	30	imp	$⊢ (ψ \land z \in pred (x, A, R)) \to ({h ↾}_{D}) (z) = h (z)$
32	25 28 31	3eqtr4d	$⊢ (ψ \land z \in pred (x, A, R)) \to ({g ↾}_{D}) (z) = ({h ↾}_{D}) (z)$
33	32	ralrimiva	$⊢ ψ \to \forall z \in pred (x, A, R) ({g ↾}_{D}) (z) = ({h ↾}_{D}) (z)$
34	9	resabs1d	$⊢ ψ \to {({g ↾}_{D}) ↾}_{pred (x, A, R)} = {g ↾}_{pred (x, A, R)}$
35	9	resabs1d	$⊢ ψ \to {({h ↾}_{D}) ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)}$
36	34 35	eqeq12d	$⊢ ψ \to ({({g ↾}_{D}) ↾}_{pred (x, A, R)} = {({h ↾}_{D}) ↾}_{pred (x, A, R)} \leftrightarrow {g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)})$
37	1 2 3 4 5 6 7	bnj1256	$⊢ φ \to \exists d \in B g Fn d$
38	4	bnj1292	$⊢ D \subseteq dom g$
39		fndm	$⊢ g Fn d \to dom g = d$
40	38 39	sseqtrid	$⊢ g Fn d \to D \subseteq d$
41		fnssres	$⊢ (g Fn d \land D \subseteq d) \to ({g ↾}_{D}) Fn D$
42	40 41	mpdan	$⊢ g Fn d \to ({g ↾}_{D}) Fn D$
43	37 42	bnj31	$⊢ φ \to \exists d \in B ({g ↾}_{D}) Fn D$
44	43	bnj1265	$⊢ φ \to ({g ↾}_{D}) Fn D$
45	7 44	bnj835	$⊢ ψ \to ({g ↾}_{D}) Fn D$
46	1 2 3 4 5 6 7	bnj1259	$⊢ φ \to \exists d \in B h Fn d$
47	4	bnj1293	$⊢ D \subseteq dom h$
48		fndm	$⊢ h Fn d \to dom h = d$
49	47 48	sseqtrid	$⊢ h Fn d \to D \subseteq d$
50		fnssres	$⊢ (h Fn d \land D \subseteq d) \to ({h ↾}_{D}) Fn D$
51	49 50	mpdan	$⊢ h Fn d \to ({h ↾}_{D}) Fn D$
52	46 51	bnj31	$⊢ φ \to \exists d \in B ({h ↾}_{D}) Fn D$
53	52	bnj1265	$⊢ φ \to ({h ↾}_{D}) Fn D$
54	7 53	bnj835	$⊢ ψ \to ({h ↾}_{D}) Fn D$
55		fvreseq	$⊢ ((({g ↾}_{D}) Fn D \land ({h ↾}_{D}) Fn D) \land pred (x, A, R) \subseteq D) \to ({({g ↾}_{D}) ↾}_{pred (x, A, R)} = {({h ↾}_{D}) ↾}_{pred (x, A, R)} \leftrightarrow \forall z \in pred (x, A, R) ({g ↾}_{D}) (z) = ({h ↾}_{D}) (z))$
56	45 54 9 55	syl21anc	$⊢ ψ \to ({({g ↾}_{D}) ↾}_{pred (x, A, R)} = {({h ↾}_{D}) ↾}_{pred (x, A, R)} \leftrightarrow \forall z \in pred (x, A, R) ({g ↾}_{D}) (z) = ({h ↾}_{D}) (z))$
57	36 56	bitr3d	$⊢ ψ \to ({g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)} \leftrightarrow \forall z \in pred (x, A, R) ({g ↾}_{D}) (z) = ({h ↾}_{D}) (z))$
58	33 57	mpbird	$⊢ ψ \to {g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)}$

Metamath Proof Explorer

Theorem bnj1280

Proof