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' ) ) )