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

Metamath Proof Explorer

Theorem bnj934

Description: Technical lemma for bnj69 . 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 bnj934.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj934.4 
|- ( ph' <-> [. p / n ]. ph )
bnj934.7 
|- ( ph" <-> [. G / f ]. ph' )
bnj934.50 
|- G e. _V
Assertion bnj934 
|- ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" )

Proof

Step Hyp Ref Expression
1 bnj934.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj934.4 
 |-  ( ph' <-> [. p / n ]. ph )
3 bnj934.7 
 |-  ( ph" <-> [. G / f ]. ph' )
4 bnj934.50 
 |-  G e. _V
5 eqtr 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ( f ` (/) ) = _pred ( X , A , R ) ) -> ( G ` (/) ) = _pred ( X , A , R ) )
6 1 5 sylan2b 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph ) -> ( G ` (/) ) = _pred ( X , A , R ) )
7 vex 
 |-  p e. _V
8 1 2 7 bnj523 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) )
9 8 1 bitr4i 
 |-  ( ph' <-> ph )
10 9 sbcbii 
 |-  ( [. G / f ]. ph' <-> [. G / f ]. ph )
11 3 10 bitri 
 |-  ( ph" <-> [. G / f ]. ph )
12 1 11 4 bnj609 
 |-  ( ph" <-> ( G ` (/) ) = _pred ( X , A , R ) )
13 6 12 sylibr 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph ) -> ph" )
14 13 ancoms 
 |-  ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" )