bnj1415

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

Proof

Step	Hyp	Ref	Expression
1		bnj1415.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1415.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1415.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1415.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1415.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1415.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1415.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1415.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1415.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		bnj1415.10	$⊢ P = ⋃ H$
11	6	simplbi	$⊢ ψ \to R FrSe A$
12	7 11	bnj835	$⊢ χ \to R FrSe A$
13	5 7	bnj1212	$⊢ χ \to x \in A$
14		eqid	$⊢ pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R) = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
15	14	bnj1414	$⊢ (R FrSe A \land x \in A) \to trCl (x, A, R) = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
16	12 13 15	syl2anc	$⊢ χ \to trCl (x, A, R) = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
17		iunun	$⊢ ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = ⋃_{y \in pred (x, A, R)} \{y\} \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
18		iunid	$⊢ ⋃_{y \in pred (x, A, R)} \{y\} = pred (x, A, R)$
19	18	uneq1i	$⊢ ⋃_{y \in pred (x, A, R)} \{y\} \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R) = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
20	17 19	eqtri	$⊢ ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
21		biid	$⊢ (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))) \leftrightarrow (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)))$
22		biid	$⊢ ((χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))) \land y \in pred (x, A, R) \land z \in (\{y\} \cup trCl (y, A, R))) \leftrightarrow ((χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))) \land y \in pred (x, A, R) \land z \in (\{y\} \cup trCl (y, A, R)))$
23	1 2 3 4 5 6 7 8 9 10 21 22	bnj1398	$⊢ χ \to ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = dom P$
24	20 23	eqtr3id	$⊢ χ \to pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R) = dom P$
25	16 24	eqtr2d	$⊢ χ \to dom P = trCl (x, A, R)$

Metamath Proof Explorer

Theorem bnj1415

Proof