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

Metamath Proof Explorer

Theorem bnj130

Description: Technical lemma for bnj151 . 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 bnj130.1 
|- ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
bnj130.2 
|- ( ph' <-> [. 1o / n ]. ph )
bnj130.3 
|- ( ps' <-> [. 1o / n ]. ps )
bnj130.4 
|- ( th' <-> [. 1o / n ]. th )
Assertion bnj130 
|- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) )

Proof

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