bnj1296

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

Proof

Step	Hyp	Ref	Expression
1		bnj1296.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1296.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1296.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1296.4	$⊢ D = dom g \cap dom h$
5		bnj1296.5	$⊢ E = \{x \in D \| g (x) \neq h (x)\}$
6		bnj1296.6	$⊢ φ \leftrightarrow (R FrSe A \land g \in C \land h \in C \land {g ↾}_{D} \neq {h ↾}_{D})$
7		bnj1296.7	$⊢ ψ \leftrightarrow (φ \land x \in E \land \forall y \in E \neg y R x)$
8		bnj1296.18	$⊢ ψ \to {g ↾}_{pred (x, A, R)} = {h ↾}_{pred (x, A, R)}$
9		bnj1296.9	$⊢ Z = ⟨x, {g ↾}_{pred (x, A, R)}⟩$
10		bnj1296.10	$⊢ K = \{g \| \exists d \in B (g Fn d \land \forall x \in d g (x) = G (Z))\}$
11		bnj1296.11	$⊢ W = ⟨x, {h ↾}_{pred (x, A, R)}⟩$
12		bnj1296.12	$⊢ L = \{h \| \exists d \in B (h Fn d \land \forall x \in d h (x) = G (W))\}$
13	8	opeq2d	$⊢ ψ \to ⟨x, {g ↾}_{pred (x, A, R)}⟩ = ⟨x, {h ↾}_{pred (x, A, R)}⟩$
14	13 9 11	3eqtr4g	$⊢ ψ \to Z = W$
15	14	fveq2d	$⊢ ψ \to G (Z) = G (W)$
16	10	bnj1436	$⊢ g \in K \to \exists d \in B (g Fn d \land \forall x \in d g (x) = G (Z))$
17		fndm	$⊢ g Fn d \to dom g = d$
18	17	anim1i	$⊢ (g Fn d \land \forall x \in d g (x) = G (Z)) \to (dom g = d \land \forall x \in d g (x) = G (Z))$
19	16 18	bnj31	$⊢ g \in K \to \exists d \in B (dom g = d \land \forall x \in d g (x) = G (Z))$
20		raleq	$⊢ dom g = d \to (\forall x \in dom g g (x) = G (Z) \leftrightarrow \forall x \in d g (x) = G (Z))$
21	20	pm5.32i	$⊢ (dom g = d \land \forall x \in dom g g (x) = G (Z)) \leftrightarrow (dom g = d \land \forall x \in d g (x) = G (Z))$
22	21	rexbii	$⊢ \exists d \in B (dom g = d \land \forall x \in dom g g (x) = G (Z)) \leftrightarrow \exists d \in B (dom g = d \land \forall x \in d g (x) = G (Z))$
23	19 22	sylibr	$⊢ g \in K \to \exists d \in B (dom g = d \land \forall x \in dom g g (x) = G (Z))$
24		simpr	$⊢ (dom g = d \land \forall x \in dom g g (x) = G (Z)) \to \forall x \in dom g g (x) = G (Z)$
25	23 24	bnj31	$⊢ g \in K \to \exists d \in B \forall x \in dom g g (x) = G (Z)$
26	25	bnj1265	$⊢ g \in K \to \forall x \in dom g g (x) = G (Z)$
27	2 3 9 10	bnj1234	$⊢ C = K$
28	26 27	eleq2s	$⊢ g \in C \to \forall x \in dom g g (x) = G (Z)$
29	6 28	bnj770	$⊢ φ \to \forall x \in dom g g (x) = G (Z)$
30	7 29	bnj835	$⊢ ψ \to \forall x \in dom g g (x) = G (Z)$
31	4	bnj1292	$⊢ D \subseteq dom g$
32	5 7	bnj1212	$⊢ ψ \to x \in D$
33	31 32	bnj1213	$⊢ ψ \to x \in dom g$
34	30 33	bnj1294	$⊢ ψ \to g (x) = G (Z)$
35	12	bnj1436	$⊢ h \in L \to \exists d \in B (h Fn d \land \forall x \in d h (x) = G (W))$
36		fndm	$⊢ h Fn d \to dom h = d$
37	36	anim1i	$⊢ (h Fn d \land \forall x \in d h (x) = G (W)) \to (dom h = d \land \forall x \in d h (x) = G (W))$
38	35 37	bnj31	$⊢ h \in L \to \exists d \in B (dom h = d \land \forall x \in d h (x) = G (W))$
39		raleq	$⊢ dom h = d \to (\forall x \in dom h h (x) = G (W) \leftrightarrow \forall x \in d h (x) = G (W))$
40	39	pm5.32i	$⊢ (dom h = d \land \forall x \in dom h h (x) = G (W)) \leftrightarrow (dom h = d \land \forall x \in d h (x) = G (W))$
41	40	rexbii	$⊢ \exists d \in B (dom h = d \land \forall x \in dom h h (x) = G (W)) \leftrightarrow \exists d \in B (dom h = d \land \forall x \in d h (x) = G (W))$
42	38 41	sylibr	$⊢ h \in L \to \exists d \in B (dom h = d \land \forall x \in dom h h (x) = G (W))$
43		simpr	$⊢ (dom h = d \land \forall x \in dom h h (x) = G (W)) \to \forall x \in dom h h (x) = G (W)$
44	42 43	bnj31	$⊢ h \in L \to \exists d \in B \forall x \in dom h h (x) = G (W)$
45	44	bnj1265	$⊢ h \in L \to \forall x \in dom h h (x) = G (W)$
46	2 3 11 12	bnj1234	$⊢ C = L$
47	45 46	eleq2s	$⊢ h \in C \to \forall x \in dom h h (x) = G (W)$
48	6 47	bnj771	$⊢ φ \to \forall x \in dom h h (x) = G (W)$
49	7 48	bnj835	$⊢ ψ \to \forall x \in dom h h (x) = G (W)$
50	4	bnj1293	$⊢ D \subseteq dom h$
51	50 32	bnj1213	$⊢ ψ \to x \in dom h$
52	49 51	bnj1294	$⊢ ψ \to h (x) = G (W)$
53	15 34 52	3eqtr4d	$⊢ ψ \to g (x) = h (x)$

Metamath Proof Explorer

Theorem bnj1296

Proof