bnj1286

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

Proof

Step	Hyp	Ref	Expression
1		bnj1286.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1286.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1286.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1286.4	$⊢ D = dom g \cap dom h$
5		bnj1286.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
6		bnj1286.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
7		bnj1286.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
8	1 2 3 4 5 6 7	bnj1256	$⊢ φ \to \exists d \in B g Fn d$
9	8	bnj1196	$⊢ φ \to \exists d (d \in B \land g Fn d)$
10	1	bnj1517	$⊢ d \in B \to \forall x \in d pred (x, A, R) \subseteq d$
11	10	adantr	$⊢ (d \in B \land g Fn d) \to \forall x \in d pred (x, A, R) \subseteq d$
12		fndm	$⊢ g Fn d \to dom g = d$
13		sseq2	$⊢ dom g = d \to (pred (x, A, R) \subseteq dom g \leftrightarrow pred (x, A, R) \subseteq d)$
14	13	raleqbi1dv	$⊢ dom g = d \to (\forall x \in dom g pred (x, A, R) \subseteq dom g \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
15	12 14	syl	$⊢ g Fn d \to (\forall x \in dom g pred (x, A, R) \subseteq dom g \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
16	15	adantl	$⊢ (d \in B \land g Fn d) \to (\forall x \in dom g pred (x, A, R) \subseteq dom g \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
17	11 16	mpbird	$⊢ (d \in B \land g Fn d) \to \forall x \in dom g pred (x, A, R) \subseteq dom g$
18	9 17	bnj593	$⊢ φ \to \exists d \forall x \in dom g pred (x, A, R) \subseteq dom g$
19	18	bnj937	$⊢ φ \to \forall x \in dom g pred (x, A, R) \subseteq dom g$
20	7 19	bnj835	$⊢ ψ \to \forall x \in dom g pred (x, A, R) \subseteq dom g$
21	5	ssrab3	$⊢ E \subseteq D$
22	4	bnj1292	$⊢ D \subseteq dom g$
23	21 22	sstri	$⊢ E \subseteq dom g$
24	23	sseli	$⊢ x \in E \to x \in dom g$
25	7 24	bnj836	$⊢ ψ \to x \in dom g$
26	20 25	bnj1294	$⊢ ψ \to pred (x, A, R) \subseteq dom g$
27	1 2 3 4 5 6 7	bnj1259	$⊢ φ \to \exists d \in B h Fn d$
28	27	bnj1196	$⊢ φ \to \exists d (d \in B \land h Fn d)$
29	10	adantr	$⊢ (d \in B \land h Fn d) \to \forall x \in d pred (x, A, R) \subseteq d$
30		fndm	$⊢ h Fn d \to dom h = d$
31		sseq2	$⊢ dom h = d \to (pred (x, A, R) \subseteq dom h \leftrightarrow pred (x, A, R) \subseteq d)$
32	31	raleqbi1dv	$⊢ dom h = d \to (\forall x \in dom h pred (x, A, R) \subseteq dom h \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
33	30 32	syl	$⊢ h Fn d \to (\forall x \in dom h pred (x, A, R) \subseteq dom h \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
34	33	adantl	$⊢ (d \in B \land h Fn d) \to (\forall x \in dom h pred (x, A, R) \subseteq dom h \leftrightarrow \forall x \in d pred (x, A, R) \subseteq d)$
35	29 34	mpbird	$⊢ (d \in B \land h Fn d) \to \forall x \in dom h pred (x, A, R) \subseteq dom h$
36	28 35	bnj593	$⊢ φ \to \exists d \forall x \in dom h pred (x, A, R) \subseteq dom h$
37	36	bnj937	$⊢ φ \to \forall x \in dom h pred (x, A, R) \subseteq dom h$
38	7 37	bnj835	$⊢ ψ \to \forall x \in dom h pred (x, A, R) \subseteq dom h$
39	4	bnj1293	$⊢ D \subseteq dom h$
40	21 39	sstri	$⊢ E \subseteq dom h$
41	40	sseli	$⊢ x \in E \to x \in dom h$
42	7 41	bnj836	$⊢ ψ \to x \in dom h$
43	38 42	bnj1294	$⊢ ψ \to pred (x, A, R) \subseteq dom h$
44	26 43	ssind	$⊢ ψ \to pred (x, A, R) \subseteq dom g \cap dom h$
45	44 4	sseqtrrdi	$⊢ ψ \to pred (x, A, R) \subseteq D$

Metamath Proof Explorer

Theorem bnj1286

Proof