bnj1445

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

Proof

Step	Hyp	Ref	Expression
1		bnj1445.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1445.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1445.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1445.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1445.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1445.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1445.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1445.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1445.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		bnj1445.10	$⊢ P = ⋃ H$
11		bnj1445.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
12		bnj1445.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
13		bnj1445.13	$⊢ W = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
14		bnj1445.14	$⊢ E = \{x\} \cup trCl (x, A, R)$
15		bnj1445.15	$⊢ χ \to P Fn trCl (x, A, R)$
16		bnj1445.16	$⊢ χ \to Q Fn (\{x\} \cup trCl (x, A, R))$
17		bnj1445.17	$⊢ θ \leftrightarrow (χ \land z \in E)$
18		bnj1445.18	$⊢ η \leftrightarrow (θ \land z \in \{x\})$
19		bnj1445.19	$⊢ ζ \leftrightarrow (θ \land z \in trCl (x, A, R))$
20		bnj1445.20	$⊢ ρ \leftrightarrow (ζ \land f \in H \land z \in dom f)$
21		bnj1445.21	$⊢ σ \leftrightarrow (ρ \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
22		bnj1445.22	$⊢ φ \leftrightarrow (σ \land d \in B \land f Fn d \land \forall x \in d f (x) = G (Y))$
23		bnj1445.23	$⊢ X = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
24		nfv	$⊢ Ⅎ d R FrSe A$
25		nfre1	$⊢ Ⅎ d \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))$
26	25	nfab	$⊢ \underline{Ⅎ} d \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
27	3 26	nfcxfr	$⊢ \underline{Ⅎ} d C$
28	27	nfcri	$⊢ Ⅎ d f \in C$
29		nfv	$⊢ Ⅎ d dom f = \{x\} \cup trCl (x, A, R)$
30	28 29	nfan	$⊢ Ⅎ d (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
31	4 30	nfxfr	$⊢ Ⅎ d τ$
32	31	nfex	$⊢ Ⅎ d \exists f τ$
33	32	nfn	$⊢ Ⅎ d \neg \exists f τ$
34		nfcv	$⊢ \underline{Ⅎ} d A$
35	33 34	nfrabw	$⊢ \underline{Ⅎ} d \{x \in A \| \neg \exists f τ\}$
36	5 35	nfcxfr	$⊢ \underline{Ⅎ} d D$
37		nfcv	$⊢ \underline{Ⅎ} d \emptyset$
38	36 37	nfne	$⊢ Ⅎ d D \neq \emptyset$
39	24 38	nfan	$⊢ Ⅎ d (R FrSe A \land D \neq \emptyset)$
40	6 39	nfxfr	$⊢ Ⅎ d ψ$
41	36	nfcri	$⊢ Ⅎ d x \in D$
42		nfv	$⊢ Ⅎ d \neg y R x$
43	36 42	nfralw	$⊢ Ⅎ d \forall y \in D \neg y R x$
44	40 41 43	nf3an	$⊢ Ⅎ d (ψ \land x \in D \land \forall y \in D \neg y R x)$
45	7 44	nfxfr	$⊢ Ⅎ d χ$
46	45	nf5ri	$⊢ χ \to \forall d χ$
47	46	bnj1351	$⊢ (χ \land z \in E) \to \forall d (χ \land z \in E)$
48	47	nf5i	$⊢ Ⅎ d (χ \land z \in E)$
49	17 48	nfxfr	$⊢ Ⅎ d θ$
50		nfv	$⊢ Ⅎ d z \in trCl (x, A, R)$
51	49 50	nfan	$⊢ Ⅎ d (θ \land z \in trCl (x, A, R))$
52	19 51	nfxfr	$⊢ Ⅎ d ζ$
53		nfcv	$⊢ \underline{Ⅎ} d pred (x, A, R)$
54		nfcv	$⊢ \underline{Ⅎ} d y$
55	54 31	nfsbcw	$⊢ Ⅎ d \underset{˙}{[} y / x \underset{˙}{]} τ$
56	8 55	nfxfr	Could not format F/ d ta' : No typesetting found for \|- F/ d ta' with typecode \|-
57	53 56	nfrex	Could not format F/ d E. y e. _pred ( x , A , R ) ta' : No typesetting found for \|- F/ d E. y e. _pred ( x , A , R ) ta' with typecode \|-
58	57	nfab	Could not format F/_ d { f \| E. y e. _pred ( x , A , R ) ta' } : No typesetting found for \|- F/_ d { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
59	9 58	nfcxfr	$⊢ \underline{Ⅎ} d H$
60	59	nfcri	$⊢ Ⅎ d f \in H$
61		nfv	$⊢ Ⅎ d z \in dom f$
62	52 60 61	nf3an	$⊢ Ⅎ d (ζ \land f \in H \land z \in dom f)$
63	20 62	nfxfr	$⊢ Ⅎ d ρ$
64	63	nf5ri	$⊢ ρ \to \forall d ρ$
65		ax-5	$⊢ y \in pred (x, A, R) \to \forall d y \in pred (x, A, R)$
66	28	nf5ri	$⊢ f \in C \to \forall d f \in C$
67		ax-5	$⊢ dom f = \{y\} \cup trCl (y, A, R) \to \forall d dom f = \{y\} \cup trCl (y, A, R)$
68	64 65 66 67	bnj982	$⊢ (ρ \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \to \forall d (ρ \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
69	21 68	hbxfrbi	$⊢ σ \to \forall d σ$

Metamath Proof Explorer

Theorem bnj1445

Proof