bnj1463

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	bnj1463.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1463.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1463.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1463.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
	bnj1463.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
	bnj1463.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
	bnj1463.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
	bnj1463.8	No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
	bnj1463.9	No typesetting found for \|- H = { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
	bnj1463.10	$⊢ P = ⋃ H$
	bnj1463.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
	bnj1463.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
	bnj1463.13	$⊢ W = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
	bnj1463.14	$⊢ E = \{x\} \cup trCl (x, A, R)$
	bnj1463.15	$⊢ χ \to Q \in V$
	bnj1463.16	$⊢ χ \to \forall z \in E Q (z) = G (W)$
	bnj1463.17	$⊢ χ \to Q Fn E$
	bnj1463.18	$⊢ χ \to E \in B$
Assertion	bnj1463	$⊢ χ \to Q \in C$

Proof

Step	Hyp	Ref	Expression
1		bnj1463.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1463.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1463.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1463.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1463.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1463.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1463.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1463.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1463.9	Could not format H = { f \| E. y e. _pred ( x , A , R ) ta' } : No typesetting found for \|- H = { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
10		bnj1463.10	$⊢ P = ⋃ H$
11		bnj1463.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
12		bnj1463.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
13		bnj1463.13	$⊢ W = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
14		bnj1463.14	$⊢ E = \{x\} \cup trCl (x, A, R)$
15		bnj1463.15	$⊢ χ \to Q \in V$
16		bnj1463.16	$⊢ χ \to \forall z \in E Q (z) = G (W)$
17		bnj1463.17	$⊢ χ \to Q Fn E$
18		bnj1463.18	$⊢ χ \to E \in B$
19	18	elexd	$⊢ χ \to E \in V$
20		eleq1	$⊢ d = E \to (d \in B \leftrightarrow E \in B)$
21		fneq2	$⊢ d = E \to (Q Fn d \leftrightarrow Q Fn E)$
22		raleq	$⊢ d = E \to (\forall z \in d Q (z) = G (W) \leftrightarrow \forall z \in E Q (z) = G (W))$
23	21 22	anbi12d	$⊢ d = E \to ((Q Fn d \land \forall z \in d Q (z) = G (W)) \leftrightarrow (Q Fn E \land \forall z \in E Q (z) = G (W)))$
24	20 23	anbi12d	$⊢ d = E \to ((d \in B \land (Q Fn d \land \forall z \in d Q (z) = G (W))) \leftrightarrow (E \in B \land (Q Fn E \land \forall z \in E Q (z) = G (W))))$
25	1	bnj1317	$⊢ w \in B \to \forall d w \in B$
26	25	nfcii	$⊢ \underline{Ⅎ} d B$
27	26	nfel2	$⊢ Ⅎ d E \in B$
28	1 2 3 4 5 6 7 8 9 10 11 12	bnj1467	$⊢ w \in Q \to \forall d w \in Q$
29	28	nfcii	$⊢ \underline{Ⅎ} d Q$
30		nfcv	$⊢ \underline{Ⅎ} d E$
31	29 30	nffn	$⊢ Ⅎ d Q Fn E$
32	1 2 3 4 5 6 7 8 9 10 11 12 13	bnj1446	$⊢ Q (z) = G (W) \to \forall d Q (z) = G (W)$
33	32	nf5i	$⊢ Ⅎ d Q (z) = G (W)$
34	30 33	nfralw	$⊢ Ⅎ d \forall z \in E Q (z) = G (W)$
35	31 34	nfan	$⊢ Ⅎ d (Q Fn E \land \forall z \in E Q (z) = G (W))$
36	27 35	nfan	$⊢ Ⅎ d (E \in B \land (Q Fn E \land \forall z \in E Q (z) = G (W)))$
37	36	nf5ri	$⊢ (E \in B \land (Q Fn E \land \forall z \in E Q (z) = G (W))) \to \forall d (E \in B \land (Q Fn E \land \forall z \in E Q (z) = G (W)))$
38	18 17 16	jca32	$⊢ χ \to (E \in B \land (Q Fn E \land \forall z \in E Q (z) = G (W)))$
39	24 37 38	bnj1465	$⊢ (χ \land E \in V) \to \exists d (d \in B \land (Q Fn d \land \forall z \in d Q (z) = G (W)))$
40	19 39	mpdan	$⊢ χ \to \exists d (d \in B \land (Q Fn d \land \forall z \in d Q (z) = G (W)))$
41		df-rex	$⊢ \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W)) \leftrightarrow \exists d (d \in B \land (Q Fn d \land \forall z \in d Q (z) = G (W)))$
42	40 41	sylibr	$⊢ χ \to \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W))$
43		nfcv	$⊢ \underline{Ⅎ} f B$
44	1 2 3 4 5 6 7 8 9 10 11 12	bnj1466	$⊢ w \in Q \to \forall f w \in Q$
45	44	nfcii	$⊢ \underline{Ⅎ} f Q$
46		nfcv	$⊢ \underline{Ⅎ} f d$
47	45 46	nffn	$⊢ Ⅎ f Q Fn d$
48	1 2 3 4 5 6 7 8 9 10 11 12 13	bnj1448	$⊢ Q (z) = G (W) \to \forall f Q (z) = G (W)$
49	48	nf5i	$⊢ Ⅎ f Q (z) = G (W)$
50	46 49	nfralw	$⊢ Ⅎ f \forall z \in d Q (z) = G (W)$
51	47 50	nfan	$⊢ Ⅎ f (Q Fn d \land \forall z \in d Q (z) = G (W))$
52	43 51	nfrexw	$⊢ Ⅎ f \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W))$
53	52	nf5ri	$⊢ \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W)) \to \forall f \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W))$
54	29	nfeq2	$⊢ Ⅎ d f = Q$
55		fneq1	$⊢ f = Q \to (f Fn d \leftrightarrow Q Fn d)$
56		fveq1	$⊢ f = Q \to f (z) = Q (z)$
57		reseq1	$⊢ f = Q \to {f ↾}_{pred (z, A, R)} = {Q ↾}_{pred (z, A, R)}$
58	57	opeq2d	$⊢ f = Q \to ⟨z, {f ↾}_{pred (z, A, R)}⟩ = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
59	58 13	eqtr4di	$⊢ f = Q \to ⟨z, {f ↾}_{pred (z, A, R)}⟩ = W$
60	59	fveq2d	$⊢ f = Q \to G (⟨z, {f ↾}_{pred (z, A, R)}⟩) = G (W)$
61	56 60	eqeq12d	$⊢ f = Q \to (f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩) \leftrightarrow Q (z) = G (W))$
62	61	ralbidv	$⊢ f = Q \to (\forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩) \leftrightarrow \forall z \in d Q (z) = G (W))$
63	55 62	anbi12d	$⊢ f = Q \to ((f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)) \leftrightarrow (Q Fn d \land \forall z \in d Q (z) = G (W)))$
64	54 63	rexbid	$⊢ f = Q \to (\exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)) \leftrightarrow \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W)))$
65	53 64 44	bnj1468	$⊢ Q \in V \to (\underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)) \leftrightarrow \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W)))$
66	15 65	syl	$⊢ χ \to (\underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)) \leftrightarrow \exists d \in B (Q Fn d \land \forall z \in d Q (z) = G (W)))$
67	42 66	mpbird	$⊢ χ \to \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩))$
68		fveq2	$⊢ x = z \to f (x) = f (z)$
69		id	$⊢ x = z \to x = z$
70		bnj602	$⊢ x = z \to pred (x, A, R) = pred (z, A, R)$
71	70	reseq2d	$⊢ x = z \to {f ↾}_{pred (x, A, R)} = {f ↾}_{pred (z, A, R)}$
72	69 71	opeq12d	$⊢ x = z \to ⟨x, {f ↾}_{pred (x, A, R)}⟩ = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
73	2 72	eqtrid	$⊢ x = z \to Y = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
74	73	fveq2d	$⊢ x = z \to G (Y) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)$
75	68 74	eqeq12d	$⊢ x = z \to (f (x) = G (Y) \leftrightarrow f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩))$
76	75	cbvralvw	$⊢ \forall x \in d f (x) = G (Y) \leftrightarrow \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩)$
77	76	anbi2i	$⊢ (f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩))$
78	77	rexbii	$⊢ \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow \exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩))$
79	78	sbcbii	$⊢ \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall z \in d f (z) = G (⟨z, {f ↾}_{pred (z, A, R)}⟩))$
80	67 79	sylibr	$⊢ χ \to \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))$
81	3	bnj1454	$⊢ Q \in V \to (Q \in C \leftrightarrow \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y)))$
82	15 81	syl	$⊢ χ \to (Q \in C \leftrightarrow \underset{˙}{[} Q / f \underset{˙}{]} \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y)))$
83	80 82	mpbird	$⊢ χ \to Q \in C$

Metamath Proof Explorer

Theorem bnj1463

Proof