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