This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )