bnj1279

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

Proof

Step	Hyp	Ref	Expression
1		bnj1279.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1279.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1279.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1279.4	$⊢ D = dom g \cap dom h$
5		bnj1279.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
6		bnj1279.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
7		bnj1279.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
8		n0	$⊢ pred (x, A, R) \cap E \neq \emptyset \leftrightarrow \exists y y \in (pred (x, A, R) \cap E)$
9		elin	$⊢ y \in (pred (x, A, R) \cap E) \leftrightarrow (y \in pred (x, A, R) \land y \in E)$
10	9	exbii	$⊢ \exists y y \in (pred (x, A, R) \cap E) \leftrightarrow \exists y (y \in pred (x, A, R) \land y \in E)$
11	8 10	sylbb	$⊢ pred (x, A, R) \cap E \neq \emptyset \to \exists y (y \in pred (x, A, R) \land y \in E)$
12		df-bnj14	$⊢ pred (x, A, R) = \{y \in A \| y R x\}$
13	12	bnj1538	$⊢ y \in pred (x, A, R) \to y R x$
14	13	anim1i	$⊢ (y \in pred (x, A, R) \land y \in E) \to (y R x \land y \in E)$
15	11 14	bnj593	$⊢ pred (x, A, R) \cap E \neq \emptyset \to \exists y (y R x \land y \in E)$
16	15	3ad2ant3	$⊢ (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \to \exists y (y R x \land y \in E)$
17		nfv	$⊢ Ⅎ y x \in E$
18		nfra1	$⊢ Ⅎ y \forall y \in E \neg y R x$
19		nfv	$⊢ Ⅎ y pred (x, A, R) \cap E \neq \emptyset$
20	17 18 19	nf3an	$⊢ Ⅎ y (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset)$
21	20	nf5ri	$⊢ (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \to \forall y (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset)$
22	16 21	bnj1275	$⊢ (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \to \exists y ((x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \land y R x \land y \in E)$
23		simp2	$⊢ ((x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \land y R x \land y \in E) \to y R x$
24		simp12	$⊢ ((x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \land y R x \land y \in E) \to \forall y \in E \neg y R x$
25		simp3	$⊢ ((x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \land y R x \land y \in E) \to y \in E$
26	24 25	bnj1294	$⊢ ((x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset) \land y R x \land y \in E) \to \neg y R x$
27	22 23 26	bnj1304	$⊢ \neg (x \in E \land \forall y \in E \neg y R x \land pred (x, A, R) \cap E \neq \emptyset)$
28	27	bnj1224	$⊢ (x \in E \land \forall y \in E \neg y R x) \to \neg pred (x, A, R) \cap E \neq \emptyset$
29		nne	$⊢ \neg pred (x, A, R) \cap E \neq \emptyset \leftrightarrow pred (x, A, R) \cap E = \emptyset$
30	28 29	sylib	$⊢ (x \in E \land \forall y \in E \neg y R x) \to pred (x, A, R) \cap E = \emptyset$

Metamath Proof Explorer

Theorem bnj1279

Proof