Theorem bnj97

Description: Technical lemma for bnj150 . 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
Hypothesis	bnj96.1	|- F = { <. (/) , _pred ( x , A , R ) >. }
Assertion	bnj97	|- ( ( R _FrSe A /\ x e. A ) -> ( F ` (/) ) = _pred ( x , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		bnj96.1	|- F = { <. (/) , _pred ( x , A , R ) >. }
2		bnj93	|- ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )
3		0ex	|- (/) e. _V
4	3	bnj519	|- ( _pred ( x , A , R ) e. _V -> Fun { <. (/) , _pred ( x , A , R ) >. } )
5	1	funeqi	|- ( Fun F <-> Fun { <. (/) , _pred ( x , A , R ) >. } )
6	4 5	sylibr	|- ( _pred ( x , A , R ) e. _V -> Fun F )
7	2 6	syl	|- ( ( R _FrSe A /\ x e. A ) -> Fun F )
8		opex	|- <. (/) , _pred ( x , A , R ) >. e. _V
9	8	snid	|- <. (/) , _pred ( x , A , R ) >. e. { <. (/) , _pred ( x , A , R ) >. }
10	9 1	eleqtrri	|- <. (/) , _pred ( x , A , R ) >. e. F
11		funopfv	|- ( Fun F -> ( <. (/) , _pred ( x , A , R ) >. e. F -> ( F ` (/) ) = _pred ( x , A , R ) ) )
12	7 10 11	mpisyl	|- ( ( R _FrSe A /\ x e. A ) -> ( F ` (/) ) = _pred ( x , A , R ) )