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

Metamath Proof Explorer

Theorem bnj125

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
Hypotheses bnj125.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj125.2 
|- ( ph' <-> [. 1o / n ]. ph )
bnj125.3 
|- ( ph" <-> [. F / f ]. ph' )
bnj125.4 
|- F = { <. (/) , _pred ( x , A , R ) >. }
Assertion bnj125 
|- ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj125.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj125.2 
 |-  ( ph' <-> [. 1o / n ]. ph )
3 bnj125.3 
 |-  ( ph" <-> [. F / f ]. ph' )
4 bnj125.4 
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
5 2 sbcbii 
 |-  ( [. F / f ]. ph' <-> [. F / f ]. [. 1o / n ]. ph )
6 bnj105 
 |-  1o e. _V
7 1 6 bnj91 
 |-  ( [. 1o / n ]. ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
8 7 sbcbii 
 |-  ( [. F / f ]. [. 1o / n ]. ph <-> [. F / f ]. ( f ` (/) ) = _pred ( x , A , R ) )
9 4 bnj95 
 |-  F e. _V
10 fveq1 
 |-  ( f = F -> ( f ` (/) ) = ( F ` (/) ) )
11 10 eqeq1d 
 |-  ( f = F -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ( F ` (/) ) = _pred ( x , A , R ) ) )
12 9 11 sbcie 
 |-  ( [. F / f ]. ( f ` (/) ) = _pred ( x , A , R ) <-> ( F ` (/) ) = _pred ( x , A , R ) )
13 8 12 bitri 
 |-  ( [. F / f ]. [. 1o / n ]. ph <-> ( F ` (/) ) = _pred ( x , A , R ) )
14 5 13 bitri 
 |-  ( [. F / f ]. ph' <-> ( F ` (/) ) = _pred ( x , A , R ) )
15 3 14 bitri 
 |-  ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) )