bnj1493

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	bnj1493.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1493.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1493.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
Assertion	bnj1493	$⊢ R FrSe A \to \forall x \in A \exists f \in C dom f = \{x\} \cup trCl (x, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj1493.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1493.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1493.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		biid	$⊢ (f \in C \land dom f = \{x\} \cup trCl (x, A, R)) \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		eqid	$⊢ \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} = \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\}$
6		biid	$⊢ (R FrSe A \land \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neq \emptyset) \leftrightarrow (R FrSe A \land \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neq \emptyset)$
7		biid	$⊢ ((R FrSe A \land \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neq \emptyset) \land x \in \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \land \forall y \in \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neg y R x) \leftrightarrow ((R FrSe A \land \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neq \emptyset) \land x \in \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \land \forall y \in \{x \in A \| \neg \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \neg y R x)$
8		biid	$⊢ \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R)) \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
9		eqid	$⊢ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} = \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\}$
10		eqid	$⊢ ⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} = ⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\}$
11		eqid	$⊢ ⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩ = ⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩$
12		eqid	$⊢ ⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \cup \{⟨x, G (⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩)⟩\} = ⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \cup \{⟨x, G (⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩)⟩\}$
13		eqid	$⊢ ⟨z, {(⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \cup \{⟨x, G (⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩)⟩\}) ↾}_{pred (z, A, R)}⟩ = ⟨z, {(⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} \cup \{⟨x, G (⟨x, {⋃ \{f \| \exists y \in pred (x, A, R) \underset{˙}{[} y / x \underset{˙}{]} (f \in C \land dom f = \{x\} \cup trCl (x, A, R))\} ↾}_{pred (x, A, R)}⟩)⟩\}) ↾}_{pred (z, A, R)}⟩$
14		eqid	$⊢ \{x\} \cup trCl (x, A, R) = \{x\} \cup trCl (x, A, R)$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	bnj1312	$⊢ R FrSe A \to \forall x \in A \exists f \in C dom f = \{x\} \cup trCl (x, A, R)$

Metamath Proof Explorer

Theorem bnj1493

Proof