Theorem bnj911

Description: Technical lemma for bnj69 . 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	bnj911.1	|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
	bnj911.2	|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
Assertion	bnj911	|- ( ( f Fn n /\ ph /\ ps ) -> A. i ( f Fn n /\ ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		bnj911.1	|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2		bnj911.2	|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3	2	bnj1095	|- ( ps -> A. i ps )
4	3	bnj1350	|- ( ( f Fn n /\ ph /\ ps ) -> A. i ( f Fn n /\ ph /\ ps ) )