bnj1253

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

Proof

Step	Hyp	Ref	Expression
1		bnj1253.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1253.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1253.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1253.4	$⊢ D = dom g \cap dom h$
5		bnj1253.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
6		bnj1253.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
7		bnj1253.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
8	6	bnj1254	$⊢ φ \to {g ↾}_{D} \neq {h ↾}_{D}$
9	1 2 3 4 5 6 7	bnj1256	$⊢ φ \to \exists d \in B g Fn d$
10	4	bnj1292	$⊢ D \subseteq dom g$
11		fndm	$⊢ g Fn d \to dom g = d$
12	10 11	sseqtrid	$⊢ g Fn d \to D \subseteq d$
13		fnssres	$⊢ (g Fn d \land D \subseteq d) \to ({g ↾}_{D}) Fn D$
14	12 13	mpdan	$⊢ g Fn d \to ({g ↾}_{D}) Fn D$
15	9 14	bnj31	$⊢ φ \to \exists d \in B ({g ↾}_{D}) Fn D$
16	15	bnj1265	$⊢ φ \to ({g ↾}_{D}) Fn D$
17	1 2 3 4 5 6 7	bnj1259	$⊢ φ \to \exists d \in B h Fn d$
18	4	bnj1293	$⊢ D \subseteq dom h$
19		fndm	$⊢ h Fn d \to dom h = d$
20	18 19	sseqtrid	$⊢ h Fn d \to D \subseteq d$
21		fnssres	$⊢ (h Fn d \land D \subseteq d) \to ({h ↾}_{D}) Fn D$
22	20 21	mpdan	$⊢ h Fn d \to ({h ↾}_{D}) Fn D$
23	17 22	bnj31	$⊢ φ \to \exists d \in B ({h ↾}_{D}) Fn D$
24	23	bnj1265	$⊢ φ \to ({h ↾}_{D}) Fn D$
25		ssid	$⊢ D \subseteq D$
26		fvreseq	$⊢ ((({g ↾}_{D}) Fn D \land ({h ↾}_{D}) Fn D) \land D \subseteq D) \to ({({g ↾}_{D}) ↾}_{D} = {({h ↾}_{D}) ↾}_{D} \leftrightarrow \forall x \in D ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x))$
27	25 26	mpan2	$⊢ (({g ↾}_{D}) Fn D \land ({h ↾}_{D}) Fn D) \to ({({g ↾}_{D}) ↾}_{D} = {({h ↾}_{D}) ↾}_{D} \leftrightarrow \forall x \in D ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x))$
28	16 24 27	syl2anc	$⊢ φ \to ({({g ↾}_{D}) ↾}_{D} = {({h ↾}_{D}) ↾}_{D} \leftrightarrow \forall x \in D ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x))$
29		residm	$⊢ {({g ↾}_{D}) ↾}_{D} = {g ↾}_{D}$
30		residm	$⊢ {({h ↾}_{D}) ↾}_{D} = {h ↾}_{D}$
31	29 30	eqeq12i	$⊢ {({g ↾}_{D}) ↾}_{D} = {({h ↾}_{D}) ↾}_{D} \leftrightarrow {g ↾}_{D} = {h ↾}_{D}$
32		df-ral	$⊢ \forall x \in D ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x) \leftrightarrow \forall x (x \in D \to ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x))$
33	28 31 32	3bitr3g	$⊢ φ \to ({g ↾}_{D} = {h ↾}_{D} \leftrightarrow \forall x (x \in D \to ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x)))$
34		fvres	$⊢ x \in D \to ({g ↾}_{D}) (x) = g (x)$
35		fvres	$⊢ x \in D \to ({h ↾}_{D}) (x) = h (x)$
36	34 35	eqeq12d	$⊢ x \in D \to (({g ↾}_{D}) (x) = ({h ↾}_{D}) (x) \leftrightarrow g (x) = h (x))$
37	36	pm5.74i	$⊢ (x \in D \to ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x)) \leftrightarrow (x \in D \to g (x) = h (x))$
38	37	albii	$⊢ \forall x (x \in D \to ({g ↾}_{D}) (x) = ({h ↾}_{D}) (x)) \leftrightarrow \forall x (x \in D \to g (x) = h (x))$
39	33 38	syl6bb	$⊢ φ \to ({g ↾}_{D} = {h ↾}_{D} \leftrightarrow \forall x (x \in D \to g (x) = h (x)))$
40	39	necon3abid	$⊢ φ \to ({g ↾}_{D} \neq {h ↾}_{D} \leftrightarrow \neg \forall x (x \in D \to g (x) = h (x)))$
41		df-rex	$⊢ \exists x \in D g (x) \neq h (x) \leftrightarrow \exists x (x \in D \land g (x) \neq h (x))$
42		pm4.61	$⊢ \neg (x \in D \to g (x) = h (x)) \leftrightarrow (x \in D \land \neg g (x) = h (x))$
43		df-ne	$⊢ g (x) \neq h (x) \leftrightarrow \neg g (x) = h (x)$
44	43	anbi2i	$⊢ (x \in D \land g (x) \neq h (x)) \leftrightarrow (x \in D \land \neg g (x) = h (x))$
45	42 44	bitr4i	$⊢ \neg (x \in D \to g (x) = h (x)) \leftrightarrow (x \in D \land g (x) \neq h (x))$
46	45	exbii	$⊢ \exists x \neg (x \in D \to g (x) = h (x)) \leftrightarrow \exists x (x \in D \land g (x) \neq h (x))$
47		exnal	$⊢ \exists x \neg (x \in D \to g (x) = h (x)) \leftrightarrow \neg \forall x (x \in D \to g (x) = h (x))$
48	41 46 47	3bitr2ri	$⊢ \neg \forall x (x \in D \to g (x) = h (x)) \leftrightarrow \exists x \in D g (x) \neq h (x)$
49	40 48	syl6bb	$⊢ φ \to ({g ↾}_{D} \neq {h ↾}_{D} \leftrightarrow \exists x \in D g (x) \neq h (x))$
50	8 49	mpbid	$⊢ φ \to \exists x \in D g (x) \neq h (x)$
51	5	neeq1i	$⊢ E \neq \emptyset \leftrightarrow \{x \in D \| g (x) \neq h (x)\} \neq \emptyset$
52		rabn0	$⊢ \{x \in D \| g (x) \neq h (x)\} \neq \emptyset \leftrightarrow \exists x \in D g (x) \neq h (x)$
53	51 52	bitri	$⊢ E \neq \emptyset \leftrightarrow \exists x \in D g (x) \neq h (x)$
54	50 53	sylibr	$⊢ φ \to E \neq \emptyset$

Metamath Proof Explorer

Theorem bnj1253

Proof