bnj1384

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

Proof

Step	Hyp	Ref	Expression
1		bnj1384.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1384.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1384.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1384.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1384.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1384.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1384.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1384.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1384.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		bnj1384.10	$⊢ P = ⋃ H$
11	1 2 3 4 8	bnj1373	Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for \|- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode \|-
12	1 2 3 4 5 6 7 8 9 10 11	bnj1371	$⊢ f \in H \to Fun f$
13	12	rgen	$⊢ \forall f \in H Fun f$
14		id	$⊢ R FrSe A \to R FrSe A$
15	1 2 3 4 5 6 7 8 9	bnj1374	$⊢ f \in H \to f \in C$
16		nfab1	Could not format F/_ f { f \| E. y e. _pred ( x , A , R ) ta' } : No typesetting found for \|- F/_ f { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
17	9 16	nfcxfr	$⊢ \underline{Ⅎ} f H$
18	17	nfcri	$⊢ Ⅎ f g \in H$
19		nfab1	$⊢ \underline{Ⅎ} f \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
20	3 19	nfcxfr	$⊢ \underline{Ⅎ} f C$
21	20	nfcri	$⊢ Ⅎ f g \in C$
22	18 21	nfim	$⊢ Ⅎ f (g \in H \to g \in C)$
23		eleq1w	$⊢ f = g \to (f \in H \leftrightarrow g \in H)$
24		eleq1w	$⊢ f = g \to (f \in C \leftrightarrow g \in C)$
25	23 24	imbi12d	$⊢ f = g \to ((f \in H \to f \in C) \leftrightarrow (g \in H \to g \in C))$
26	22 25 15	chvarfv	$⊢ g \in H \to g \in C$
27		eqid	$⊢ dom f \cap dom g = dom f \cap dom g$
28	1 2 3 27	bnj1326	$⊢ (R FrSe A \land f \in C \land g \in C) \to {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}$
29	14 15 26 28	syl3an	$⊢ (R FrSe A \land f \in H \land g \in H) \to {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}$
30	29	3expib	$⊢ R FrSe A \to ((f \in H \land g \in H) \to {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)})$
31	30	ralrimivv	$⊢ R FrSe A \to \forall f \in H \forall g \in H {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}$
32		biid	$⊢ \forall f \in H Fun f \leftrightarrow \forall f \in H Fun f$
33		biid	$⊢ (\forall f \in H Fun f \land \forall f \in H \forall g \in H {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}) \leftrightarrow (\forall f \in H Fun f \land \forall f \in H \forall g \in H {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)})$
34	9	bnj1317	$⊢ z \in H \to \forall f z \in H$
35	32 27 33 34	bnj1386	$⊢ (\forall f \in H Fun f \land \forall f \in H \forall g \in H {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}) \to Fun ⋃ H$
36	13 31 35	sylancr	$⊢ R FrSe A \to Fun ⋃ H$
37	10	funeqi	$⊢ Fun P \leftrightarrow Fun ⋃ H$
38	36 37	sylibr	$⊢ R FrSe A \to Fun P$

Metamath Proof Explorer

Theorem bnj1384

Proof