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

Metamath Proof Explorer

Theorem bnj207

Description: Technical lemma for bnj852 . 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 bnj207.1 
|- ( ch <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
bnj207.2 
|- ( ph' <-> [. M / n ]. ph )
bnj207.3 
|- ( ps' <-> [. M / n ]. ps )
bnj207.4 
|- ( ch' <-> [. M / n ]. ch )
bnj207.5 
|- M e. _V
Assertion bnj207 
|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )

Proof

Step Hyp Ref Expression
1 bnj207.1 
 |-  ( ch <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
2 bnj207.2 
 |-  ( ph' <-> [. M / n ]. ph )
3 bnj207.3 
 |-  ( ps' <-> [. M / n ]. ps )
4 bnj207.4 
 |-  ( ch' <-> [. M / n ]. ch )
5 bnj207.5 
 |-  M e. _V
6 1 sbcbii 
 |-  ( [. M / n ]. ch <-> [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
7 nfv 
 |-  F/ n ( R _FrSe A /\ x e. A )
8 7 sbc19.21g 
 |-  ( M e. _V -> ( [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) ) ) )
9 5 8 ax-mp 
 |-  ( [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) ) )
10 5 bnj89 
 |-  ( [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) <-> E! f [. M / n ]. ( f Fn n /\ ph /\ ps ) )
11 5 bnj90 
 |-  ( [. M / n ]. f Fn n <-> f Fn M )
12 11 bicomi 
 |-  ( f Fn M <-> [. M / n ]. f Fn n )
13 12 2 3 5 bnj206 
 |-  ( [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> ( f Fn M /\ ph' /\ ps' ) )
14 13 eubii 
 |-  ( E! f [. M / n ]. ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) )
15 10 14 bitri 
 |-  ( [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) <-> E! f ( f Fn M /\ ph' /\ ps' ) )
16 15 imbi2i 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> [. M / n ]. E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )
17 9 16 bitri 
 |-  ( [. M / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )
18 6 17 bitri 
 |-  ( [. M / n ]. ch <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )
19 4 18 bitri 
 |-  ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )