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

Metamath Proof Explorer

Theorem bnj124

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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj124.1 
|- F = { <. (/) , _pred ( x , A , R ) >. }
bnj124.2 
|- ( ph" <-> [. F / f ]. ph' )
bnj124.3 
|- ( ps" <-> [. F / f ]. ps' )
bnj124.4 
|- ( ze" <-> [. F / f ]. ze' )
bnj124.5 
|- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
Assertion bnj124 
|- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )

Proof

Step Hyp Ref Expression
1 bnj124.1 
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
2 bnj124.2 
 |-  ( ph" <-> [. F / f ]. ph' )
3 bnj124.3 
 |-  ( ps" <-> [. F / f ]. ps' )
4 bnj124.4 
 |-  ( ze" <-> [. F / f ]. ze' )
5 bnj124.5 
 |-  ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
6 5 sbcbii 
 |-  ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
7 1 bnj95 
 |-  F e. _V
8 nfv 
 |-  F/ f ( R _FrSe A /\ x e. A )
9 8 sbc19.21g 
 |-  ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) )
10 7 9 ax-mp 
 |-  ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) )
11 fneq1 
 |-  ( f = z -> ( f Fn 1o <-> z Fn 1o ) )
12 fneq1 
 |-  ( z = F -> ( z Fn 1o <-> F Fn 1o ) )
13 11 12 sbcie2g 
 |-  ( F e. _V -> ( [. F / f ]. f Fn 1o <-> F Fn 1o ) )
14 7 13 ax-mp 
 |-  ( [. F / f ]. f Fn 1o <-> F Fn 1o )
15 14 bicomi 
 |-  ( F Fn 1o <-> [. F / f ]. f Fn 1o )
16 15 2 3 7 bnj206 
 |-  ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) )
17 16 imbi2i 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )
18 6 10 17 3bitri 
 |-  ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )
19 4 18 bitri 
 |-  ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )