bnj1523

Description: Technical lemma for bnj1522 . 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	bnj1523.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1523.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1523.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1523.4	$⊢ F = ⋃ C$
	bnj1523.5	$⊢ φ \leftrightarrow (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩))$
	bnj1523.6	$⊢ ψ \leftrightarrow (φ \land F \neq H)$
	bnj1523.7	$⊢ χ \leftrightarrow (ψ \land x \in A \land F (x) \neq H (x))$
	bnj1523.8	$⊢ D = \{x \in A \| F (x) \neq H (x)\}$
	bnj1523.9	$⊢ θ \leftrightarrow (χ \land y \in D \land \forall z \in D \neg z R y)$
Assertion	bnj1523	$⊢ (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \to F = H$

Proof

Step	Hyp	Ref	Expression
1		bnj1523.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1523.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1523.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1523.4	$⊢ F = ⋃ C$
5		bnj1523.5	$⊢ φ \leftrightarrow (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩))$
6		bnj1523.6	$⊢ ψ \leftrightarrow (φ \land F \neq H)$
7		bnj1523.7	$⊢ χ \leftrightarrow (ψ \land x \in A \land F (x) \neq H (x))$
8		bnj1523.8	$⊢ D = \{x \in A \| F (x) \neq H (x)\}$
9		bnj1523.9	$⊢ θ \leftrightarrow (χ \land y \in D \land \forall z \in D \neg z R y)$
10	1 2 3 4	bnj60	$⊢ R FrSe A \to F Fn A$
11	5 10	bnj835	$⊢ φ \to F Fn A$
12	6 11	bnj832	$⊢ ψ \to F Fn A$
13	7 12	bnj835	$⊢ χ \to F Fn A$
14	9 13	bnj835	$⊢ θ \to F Fn A$
15	5	simp2bi	$⊢ φ \to H Fn A$
16	6 15	bnj832	$⊢ ψ \to H Fn A$
17	7 16	bnj835	$⊢ χ \to H Fn A$
18	9 17	bnj835	$⊢ θ \to H Fn A$
19		bnj213	$⊢ pred (y, A, R) \subseteq A$
20	19	a1i	$⊢ θ \to pred (y, A, R) \subseteq A$
21	9	simp3bi	$⊢ θ \to \forall z \in D \neg z R y$
22	21	bnj1211	$⊢ θ \to \forall z (z \in D \to \neg z R y)$
23		con2b	$⊢ (z \in D \to \neg z R y) \leftrightarrow (z R y \to \neg z \in D)$
24	23	albii	$⊢ \forall z (z \in D \to \neg z R y) \leftrightarrow \forall z (z R y \to \neg z \in D)$
25	22 24	sylib	$⊢ θ \to \forall z (z R y \to \neg z \in D)$
26		bnj1418	$⊢ z \in pred (y, A, R) \to z R y$
27	26	imim1i	$⊢ (z R y \to \neg z \in D) \to (z \in pred (y, A, R) \to \neg z \in D)$
28	27	alimi	$⊢ \forall z (z R y \to \neg z \in D) \to \forall z (z \in pred (y, A, R) \to \neg z \in D)$
29	25 28	syl	$⊢ θ \to \forall z (z \in pred (y, A, R) \to \neg z \in D)$
30	29	bnj1142	$⊢ θ \to \forall z \in pred (y, A, R) \neg z \in D$
31	1	bnj1309	$⊢ w \in B \to \forall x w \in B$
32	3 31	bnj1307	$⊢ w \in C \to \forall x w \in C$
33	32	nfcii	$⊢ \underline{Ⅎ} x C$
34	33	nfuni	$⊢ \underline{Ⅎ} x ⋃ C$
35	4 34	nfcxfr	$⊢ \underline{Ⅎ} x F$
36	35	nfcrii	$⊢ w \in F \to \forall x w \in F$
37	8 36	bnj1534	$⊢ D = \{z \in A \| F (z) \neq H (z)\}$
38	30 19 37	bnj1533	$⊢ θ \to \forall z \in pred (y, A, R) F (z) = H (z)$
39	14 18 20 38	bnj1536	$⊢ θ \to {F ↾}_{pred (y, A, R)} = {H ↾}_{pred (y, A, R)}$
40	39	opeq2d	$⊢ θ \to ⟨y, {F ↾}_{pred (y, A, R)}⟩ = ⟨y, {H ↾}_{pred (y, A, R)}⟩$
41	40	fveq2d	$⊢ θ \to G (⟨y, {F ↾}_{pred (y, A, R)}⟩) = G (⟨y, {H ↾}_{pred (y, A, R)}⟩)$
42	1 2 3 4	bnj1500	$⊢ R FrSe A \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$
43	5 42	bnj835	$⊢ φ \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$
44	6 43	bnj832	$⊢ ψ \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$
45	7 44	bnj835	$⊢ χ \to \forall x \in A F (x) = G (⟨x, {F ↾}_{pred (x, A, R)}⟩)$
46	45 36	bnj1529	$⊢ χ \to \forall y \in A F (y) = G (⟨y, {F ↾}_{pred (y, A, R)}⟩)$
47	9 46	bnj835	$⊢ θ \to \forall y \in A F (y) = G (⟨y, {F ↾}_{pred (y, A, R)}⟩)$
48	8	ssrab3	$⊢ D \subseteq A$
49	9	simp2bi	$⊢ θ \to y \in D$
50	48 49	bnj1213	$⊢ θ \to y \in A$
51	47 50	bnj1294	$⊢ θ \to F (y) = G (⟨y, {F ↾}_{pred (y, A, R)}⟩)$
52	5	simp3bi	$⊢ φ \to \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)$
53	6 52	bnj832	$⊢ ψ \to \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)$
54	7 53	bnj835	$⊢ χ \to \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)$
55		ax-5	$⊢ v \in H \to \forall x v \in H$
56	54 55	bnj1529	$⊢ χ \to \forall y \in A H (y) = G (⟨y, {H ↾}_{pred (y, A, R)}⟩)$
57	9 56	bnj835	$⊢ θ \to \forall y \in A H (y) = G (⟨y, {H ↾}_{pred (y, A, R)}⟩)$
58	57 50	bnj1294	$⊢ θ \to H (y) = G (⟨y, {H ↾}_{pred (y, A, R)}⟩)$
59	41 51 58	3eqtr4d	$⊢ θ \to F (y) = H (y)$
60	8 36	bnj1534	$⊢ D = \{y \in A \| F (y) \neq H (y)\}$
61	60	bnj1538	$⊢ y \in D \to F (y) \neq H (y)$
62	9 61	bnj836	$⊢ θ \to F (y) \neq H (y)$
63	62	neneqd	$⊢ θ \to \neg F (y) = H (y)$
64	59 63	pm2.65i	$⊢ \neg θ$
65	64	nex	$⊢ \neg \exists y θ$
66	5	simp1bi	$⊢ φ \to R FrSe A$
67	6 66	bnj832	$⊢ ψ \to R FrSe A$
68	7 67	bnj835	$⊢ χ \to R FrSe A$
69	48	a1i	$⊢ χ \to D \subseteq A$
70	7	simp2bi	$⊢ χ \to x \in A$
71	7	simp3bi	$⊢ χ \to F (x) \neq H (x)$
72	8	reqabi	$⊢ x \in D \leftrightarrow (x \in A \land F (x) \neq H (x))$
73	70 71 72	sylanbrc	$⊢ χ \to x \in D$
74	73	ne0d	$⊢ χ \to D \neq \emptyset$
75		bnj69	$⊢ (R FrSe A \land D \subseteq A \land D \neq \emptyset) \to \exists y \in D \forall z \in D \neg z R y$
76	68 69 74 75	syl3anc	$⊢ χ \to \exists y \in D \forall z \in D \neg z R y$
77	76 9	bnj1209	$⊢ χ \to \exists y θ$
78	65 77	mto	$⊢ \neg χ$
79	78	nex	$⊢ \neg \exists x χ$
80	6	simprbi	$⊢ ψ \to F \neq H$
81	12 16 80 36	bnj1542	$⊢ ψ \to \exists x \in A F (x) \neq H (x)$
82	1 2 3 4 5 6	bnj1525	$⊢ ψ \to \forall x ψ$
83	81 7 82	bnj1521	$⊢ ψ \to \exists x χ$
84	79 83	mto	$⊢ \neg ψ$
85	6 84	bnj1541	$⊢ φ \to F = H$
86	5 85	sylbir	$⊢ (R FrSe A \land H Fn A \land \forall x \in A H (x) = G (⟨x, {H ↾}_{pred (x, A, R)}⟩)) \to F = H$

Metamath Proof Explorer

Theorem bnj1523

Proof