bnj1311

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	bnj1311.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1311.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1311.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1311.4	$⊢ D = dom g \cap dom h$
Assertion	bnj1311	$⊢ (R FrSe A \land g \in C \land h \in C) \to {g ↾}_{D} = {h ↾}_{D}$

Proof

Step	Hyp	Ref	Expression
1		bnj1311.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1311.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1311.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1311.4	$⊢ D = dom g \cap dom h$
5		biid	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
6	5	bnj1232	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to R FrSe A$
7		ssrab2	$⊢ \{x \in D \| g (x) \neq h (x)\} \subseteq D$
8	5	bnj1235	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to g \in C$
9		eqid	$⊢ ⟨x, {g ↾}_{pred (x, A, R)}⟩ = ⟨x, {g ↾}_{pred (x, A, R)}⟩$
10		eqid	$⊢ \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} = \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\}$
11	2 3 9 10	bnj1234	$⊢ C = \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\}$
12	8 11	eleqtrdi	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\}$
13		abid	$⊢ g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} \leftrightarrow \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))$
14	13	bnj1238	$⊢ g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} \to \exists d \in B g Fn d$
15	14	bnj1196	$⊢ g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} \to \exists d (d \in B \land g Fn d)$
16	1	eqabri	$⊢ d \in B \leftrightarrow (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)$
17	16	simplbi	$⊢ d \in B \to d \subseteq A$
18		fndm	$⊢ g Fn d \to dom g = d$
19	17 18	bnj1241	$⊢ (d \in B \land g Fn d) \to dom g \subseteq A$
20	15 19	bnj593	$⊢ g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} \to \exists d dom g \subseteq A$
21	20	bnj937	$⊢ g \in \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (⟨x, {g ↾}_{pred (x, A, R)}⟩))\} \to dom g \subseteq A$
22		ssinss1	$⊢ dom g \subseteq A \to dom g \cap dom h \subseteq A$
23	12 21 22	3syl	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to dom g \cap dom h \subseteq A$
24	4 23	eqsstrid	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to D \subseteq A$
25	7 24	sstrid	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to \{x \in D \| g (x) \neq h (x)\} \subseteq A$
26		eqid	$⊢ \{x \in D \| g (x) \neq h (x)\} = \{x \in D \| g (x) \neq h (x)\}$
27		biid	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \leftrightarrow ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x)$
28	1 2 3 4 26 5 27	bnj1253	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to \{x \in D \| g (x) \neq h (x)\} \neq \emptyset$
29		nfrab1	$⊢ \underline{Ⅎ} x \{x \in D \| g (x) \neq h (x)\}$
30	29	nfcrii	$⊢ z \in \{x \in D \| g (x) \neq h (x)\} \to \forall x z \in \{x \in D \| g (x) \neq h (x)\}$
31	30	bnj1228	$⊢ (R FrSe A \land \{x \in D \| g (x) \neq h (x)\} \subseteq A \land \{x \in D \| g (x) \neq h (x)\} \neq \emptyset) \to \exists x \in \{x \in D \| g (x) \neq h (x)\} \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x$
32	6 25 28 31	syl3anc	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to \exists x \in \{x \in D \| g (x) \neq h (x)\} \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x$
33		ax-5	$⊢ R FrSe A \to \forall x R FrSe A$
34	1	bnj1309	$⊢ w \in B \to \forall x w \in B$
35	3 34	bnj1307	$⊢ w \in C \to \forall x w \in C$
36	35	hblem	$⊢ g \in C \to \forall x g \in C$
37	35	hblem	$⊢ h \in C \to \forall x h \in C$
38		ax-5	$⊢ {g ↾}_{D} \neq {h ↾}_{D} \to \forall x {g ↾}_{D} \neq {h ↾}_{D}$
39	33 36 37 38	bnj982	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to \forall x (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
40	32 27 39	bnj1521	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \to \exists x ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x)$
41		simp2	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to x \in \{x \in D \| g (x) \neq h (x)\}$
42	1 2 3 4 26 5 27	bnj1279	$⊢ (x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to pred (x, A, R) \cap \{x \in D \| g (x) \neq h (x)\} = \emptyset$
43	42	3adant1	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to pred (x, A, R) \cap \{x \in D \| g (x) \neq h (x)\} = \emptyset$
44	1 2 3 4 26 5 27 43	bnj1280	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to {g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)}$
45		eqid	$⊢ ⟨x, {h ↾}_{pred (x, A, R)}⟩ = ⟨x, {h ↾}_{pred (x, A, R)}⟩$
46		eqid	$⊢ \{h \| \exists d \in B (h Fn d \land \forall x \in d h (x) = G (⟨x, {h ↾}_{pred (x, A, R)}⟩))\} = \{h \| \exists d \in B (h Fn d \land \forall x \in d h (x) = G (⟨x, {h ↾}_{pred (x, A, R)}⟩))\}$
47	1 2 3 4 26 5 27 44 9 10 45 46	bnj1296	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to g (x) = h (x)$
48	26	bnj1538	$⊢ x \in \{x \in D \| g (x) \neq h (x)\} \to g (x) \neq h (x)$
49	48	necon2bi	$⊢ g (x) = h (x) \to \neg x \in \{x \in D \| g (x) \neq h (x)\}$
50	47 49	syl	$⊢ ((R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \land x \in \{x \in D \| g (x) \neq h (x)\} \land \forall y \in \{x \in D \| g (x) \neq h (x)\} \neg y R x) \to \neg x \in \{x \in D \| g (x) \neq h (x)\}$
51	40 41 50	bnj1304	$⊢ \neg (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
52		df-bnj17	$⊢ (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D}) \leftrightarrow ((R FrSe A \land g \in C \land h \in C) \land {g ↾}_{D} \neq {h ↾}_{D})$
53	51 52	mtbi	$⊢ \neg ((R FrSe A \land g \in C \land h \in C) \land {g ↾}_{D} \neq {h ↾}_{D})$
54	53	imnani	$⊢ (R FrSe A \land g \in C \land h \in C) \to \neg {g ↾}_{D} \neq {h ↾}_{D}$
55		nne	$⊢ \neg {g ↾}_{D} \neq {h ↾}_{D} \leftrightarrow {g ↾}_{D} = {h ↾}_{D}$
56	54 55	sylib	$⊢ (R FrSe A \land g \in C \land h \in C) \to {g ↾}_{D} = {h ↾}_{D}$

Metamath Proof Explorer

Theorem bnj1311

Proof