bnj1423

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

Proof

Step	Hyp	Ref	Expression
1		bnj1423.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1423.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1423.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1423.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1423.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1423.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1423.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1423.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1423.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		bnj1423.10	$⊢ P = ⋃ H$
11		bnj1423.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
12		bnj1423.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
13		bnj1423.13	$⊢ W = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
14		bnj1423.14	$⊢ E = \{x\} \cup trCl (x, A, R)$
15		bnj1423.15	$⊢ χ \to P Fn trCl (x, A, R)$
16		bnj1423.16	$⊢ χ \to Q Fn (\{x\} \cup trCl (x, A, R))$
17		biid	$⊢ (χ \land z \in E) \leftrightarrow (χ \land z \in E)$
18		biid	$⊢ ((χ \land z \in E) \land z \in \{x\}) \leftrightarrow ((χ \land z \in E) \land z \in \{x\})$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	bnj1442	$⊢ ((χ \land z \in E) \land z \in \{x\}) \to Q (z) = G (W)$
20		biid	$⊢ ((χ \land z \in E) \land z \in trCl (x, A, R)) \leftrightarrow ((χ \land z \in E) \land z \in trCl (x, A, R))$
21		biid	$⊢ (((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f) \leftrightarrow (((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f)$
22		biid	$⊢ ((((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f) \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \leftrightarrow ((((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f) \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
23		biid	$⊢ (((((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f) \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \land d \in B \land f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow (((((χ \land z \in E) \land z \in trCl (x, A, R)) \land f \in H \land z \in dom f) \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \land d \in B \land f Fn d \land \forall x \in d f (x) = G (Y))$
24		eqid	$⊢ ⟨z, {f ↾}_{pred (z, A, R)}⟩ = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 20 21 22 23 24	bnj1450	$⊢ ((χ \land z \in E) \land z \in trCl (x, A, R)) \to Q (z) = G (W)$
26	14	bnj1424	$⊢ z \in E \to (z \in \{x\} \lor z \in trCl (x, A, R))$
27	26	adantl	$⊢ (χ \land z \in E) \to (z \in \{x\} \lor z \in trCl (x, A, R))$
28	19 25 27	mpjaodan	$⊢ (χ \land z \in E) \to Q (z) = G (W)$
29	28	ralrimiva	$⊢ χ \to \forall z \in E Q (z) = G (W)$

Metamath Proof Explorer

Theorem bnj1423

Proof